./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-145.smt2 .


--------------------------------------------------------------------------------


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:53,501 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:53,607 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b8c87ffd-bc4d-4ff7-a45d-73b29d08e99f/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:53,613 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:53,613 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:53,655 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:53,657 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:53,657 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:53,658 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:53,658 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:53,659 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:53,659 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:53,659 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:53,659 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:53,659 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:53,662 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:53,662 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:53,662 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:53,662 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:53,662 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:53,662 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:53,663 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:53,663 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:53,663 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:53,663 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:53,664 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:53,664 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:54,060 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:54,073 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:54,078 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:54,079 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:54,080 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:54,084 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b8c87ffd-bc4d-4ff7-a45d-73b29d08e99f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-145.smt2
[2025-04-28 21:21:54,085 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:54,092 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:54,322 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b8c87ffd-bc4d-4ff7-a45d-73b29d08e99f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-145.smt2
[2025-04-28 21:21:54,329 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:54,331 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:54,334 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:54,334 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:54,335 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:54,338 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,369 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54 Unit
[2025-04-28 21:21:54,369 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:54,370 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:54,370 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:54,370 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:54,391 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,392 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,421 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,422 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,424 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,425 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,427 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,429 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,429 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,451 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:54,452 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:54,452 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:54,452 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:54,457 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (1/1) ...
[2025-04-28 21:21:54,462 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:54,482 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,503 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:54,507 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,524 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:54,524 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:54,524 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:54,524 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:54,525 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:54,525 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:54,525 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:54,525 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:54,525 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:54,592 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:54,594 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:54,734 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:54,734 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:54,751 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:54,752 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:54,753 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:54 BoogieIcfgContainer
[2025-04-28 21:21:54,753 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:54,758 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:54,759 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:54,763 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:54,765 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:54" (1/3) ...
[2025-04-28 21:21:54,766 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6bc81423 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:54, skipping insertion in model container
[2025-04-28 21:21:54,766 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:54" (2/3) ...
[2025-04-28 21:21:54,766 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6bc81423 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:54, skipping insertion in model container
[2025-04-28 21:21:54,766 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:54" (3/3) ...
[2025-04-28 21:21:54,768 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:54,787 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:54,792 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 15 locations, 25 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:54,856 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:54,876 INFO  L340      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=None, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@288c4bfe, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:54,877 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:54,882 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 15 states, 6 states have (on average 1.6666666666666667) internal successors, (10), 10 states have internal predecessors, (10), 5 states have call successors, (5), 2 states have call predecessors, (5), 2 states have return successors, (5), 3 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:54,893 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:54,894 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,895 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,896 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,904 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,905 INFO  L85        PathProgramCache]: Analyzing trace with hash -1122768265, now seen corresponding path program 1 times
[2025-04-28 21:21:54,915 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,915 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1863326163]
[2025-04-28 21:21:54,916 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,917 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,958 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:54,983 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:54,983 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,983 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,164 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:55,165 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,166 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1863326163]
[2025-04-28 21:21:55,167 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1863326163] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,169 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,173 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:55,175 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [560902155]
[2025-04-28 21:21:55,175 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,180 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:55,180 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,211 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:55,212 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:55,213 INFO  L87              Difference]: Start difference. First operand  has 15 states, 6 states have (on average 1.6666666666666667) internal successors, (10), 10 states have internal predecessors, (10), 5 states have call successors, (5), 2 states have call predecessors, (5), 2 states have return successors, (5), 3 states have call predecessors, (5), 5 states have call successors, (5) Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:55,311 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,311 INFO  L93              Difference]: Finished difference Result 15 states and 22 transitions.
[2025-04-28 21:21:55,314 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:55,316 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:55,316 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,327 INFO  L225             Difference]: With dead ends: 15
[2025-04-28 21:21:55,328 INFO  L226             Difference]: Without dead ends: 15
[2025-04-28 21:21:55,331 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:55,338 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 1 mSDsluCounter, 19 mSDsCounter, 0 mSdLazyCounter, 16 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 34 SdHoareTripleChecker+Invalid, 16 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 16 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,340 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 34 Invalid, 16 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 16 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:55,356 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15 states.
[2025-04-28 21:21:55,385 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15 to 15.
[2025-04-28 21:21:55,386 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 15 states, 6 states have (on average 1.5) internal successors, (9), 9 states have internal predecessors, (9), 5 states have call successors, (5), 2 states have call predecessors, (5), 3 states have return successors, (8), 3 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:55,392 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 15 states to 15 states and 22 transitions.
[2025-04-28 21:21:55,396 INFO  L79                 Accepts]: Start accepts. Automaton has 15 states and 22 transitions. Word has length 9
[2025-04-28 21:21:55,397 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,397 INFO  L485      AbstractCegarLoop]: Abstraction has 15 states and 22 transitions.
[2025-04-28 21:21:55,399 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:55,399 INFO  L278                IsEmpty]: Start isEmpty. Operand 15 states and 22 transitions.
[2025-04-28 21:21:55,401 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:55,402 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,402 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,402 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:55,403 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,403 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,405 INFO  L85        PathProgramCache]: Analyzing trace with hash -1863190075, now seen corresponding path program 1 times
[2025-04-28 21:21:55,405 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,405 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [528854449]
[2025-04-28 21:21:55,405 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,406 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,420 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:55,452 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:55,452 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,452 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,758 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:55,758 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,758 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [528854449]
[2025-04-28 21:21:55,758 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [528854449] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,759 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [574241008]
[2025-04-28 21:21:55,759 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,759 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,762 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,765 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:55,769 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,830 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:55,857 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:55,857 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,857 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,860 INFO  L256         TraceCheckSpWp]: Trace formula consists of 59 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,869 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,199 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:56,200 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,786 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:56,786 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [574241008] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,786 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,786 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 11
[2025-04-28 21:21:56,787 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1890305493]
[2025-04-28 21:21:56,787 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,788 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:56,788 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,789 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:56,789 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=32, Invalid=78, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:56,790 INFO  L87              Difference]: Start difference. First operand 15 states and 22 transitions. Second operand  has 11 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 10 states have internal predecessors, (13), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:57,012 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,013 INFO  L93              Difference]: Finished difference Result 21 states and 36 transitions.
[2025-04-28 21:21:57,013 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:57,014 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 10 states have internal predecessors, (13), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 13
[2025-04-28 21:21:57,014 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,015 INFO  L225             Difference]: With dead ends: 21
[2025-04-28 21:21:57,015 INFO  L226             Difference]: Without dead ends: 21
[2025-04-28 21:21:57,015 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 22 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 13 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=39, Invalid=93, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:57,016 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 5 mSDsluCounter, 35 mSDsCounter, 0 mSdLazyCounter, 71 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 51 SdHoareTripleChecker+Invalid, 84 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 71 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,017 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 51 Invalid, 84 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 71 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:57,020 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 21 states.
[2025-04-28 21:21:57,031 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 21 to 17.
[2025-04-28 21:21:57,032 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 17 states, 7 states have (on average 1.4285714285714286) internal successors, (10), 10 states have internal predecessors, (10), 5 states have call successors, (5), 2 states have call predecessors, (5), 4 states have return successors, (11), 4 states have call predecessors, (11), 5 states have call successors, (11)
[2025-04-28 21:21:57,033 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 26 transitions.
[2025-04-28 21:21:57,033 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 26 transitions. Word has length 13
[2025-04-28 21:21:57,033 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,033 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 26 transitions.
[2025-04-28 21:21:57,033 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 10 states have internal predecessors, (13), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:57,034 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 26 transitions.
[2025-04-28 21:21:57,034 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:57,034 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,035 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,041 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:57,239 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,240 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,240 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,240 INFO  L85        PathProgramCache]: Analyzing trace with hash -2108440928, now seen corresponding path program 1 times
[2025-04-28 21:21:57,240 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,241 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [339851208]
[2025-04-28 21:21:57,241 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,241 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,246 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:57,255 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:57,255 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,255 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,372 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:57,372 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,373 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [339851208]
[2025-04-28 21:21:57,373 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [339851208] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,373 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1728189153]
[2025-04-28 21:21:57,373 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,373 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,376 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,379 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:57,382 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,420 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:57,433 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:57,433 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,433 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,434 INFO  L256         TraceCheckSpWp]: Trace formula consists of 59 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,437 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,537 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:57,537 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,435 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:58,435 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1728189153] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,435 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:58,435 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6, 6] total 11
[2025-04-28 21:21:58,435 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1655091129]
[2025-04-28 21:21:58,436 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,436 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:58,437 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,438 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:58,438 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=84, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:58,439 INFO  L87              Difference]: Start difference. First operand 17 states and 26 transitions. Second operand  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:58,542 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,543 INFO  L93              Difference]: Finished difference Result 19 states and 30 transitions.
[2025-04-28 21:21:58,543 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:58,544 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-04-28 21:21:58,544 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,545 INFO  L225             Difference]: With dead ends: 19
[2025-04-28 21:21:58,546 INFO  L226             Difference]: Without dead ends: 19
[2025-04-28 21:21:58,547 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 31 GetRequests, 21 SyntacticMatches, 1 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=26, Invalid=84, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:58,548 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 2 mSDsluCounter, 23 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 39 SdHoareTripleChecker+Invalid, 45 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,548 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 39 Invalid, 45 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:58,549 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 19 states.
[2025-04-28 21:21:58,556 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 19 to 19.
[2025-04-28 21:21:58,557 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 19 states, 8 states have (on average 1.375) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 2 states have call predecessors, (5), 5 states have return successors, (14), 5 states have call predecessors, (14), 5 states have call successors, (14)
[2025-04-28 21:21:58,558 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 19 states to 19 states and 30 transitions.
[2025-04-28 21:21:58,558 INFO  L79                 Accepts]: Start accepts. Automaton has 19 states and 30 transitions. Word has length 13
[2025-04-28 21:21:58,558 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,558 INFO  L485      AbstractCegarLoop]: Abstraction has 19 states and 30 transitions.
[2025-04-28 21:21:58,559 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:58,559 INFO  L278                IsEmpty]: Start isEmpty. Operand 19 states and 30 transitions.
[2025-04-28 21:21:58,560 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:58,560 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,560 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,566 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:58,764 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,764 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,765 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,765 INFO  L85        PathProgramCache]: Analyzing trace with hash 1548248505, now seen corresponding path program 1 times
[2025-04-28 21:21:58,765 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,765 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [276275039]
[2025-04-28 21:21:58,765 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,765 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,771 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:58,779 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:58,779 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,780 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,918 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:58,919 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,919 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [276275039]
[2025-04-28 21:21:58,919 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [276275039] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,919 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [511168914]
[2025-04-28 21:21:58,919 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,920 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,924 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:58,926 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:58,929 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,977 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:58,992 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:58,992 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,992 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,993 INFO  L256         TraceCheckSpWp]: Trace formula consists of 63 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,994 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:59,115 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:59,115 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,881 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:59,881 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [511168914] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,881 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,881 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 11
[2025-04-28 21:21:59,881 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1471323857]
[2025-04-28 21:21:59,881 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,882 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:59,882 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,882 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:59,883 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=85, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:59,883 INFO  L87              Difference]: Start difference. First operand 19 states and 30 transitions. Second operand  has 11 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 10 states have internal predecessors, (13), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:22:00,054 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,054 INFO  L93              Difference]: Finished difference Result 27 states and 47 transitions.
[2025-04-28 21:22:00,055 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:00,055 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 10 states have internal predecessors, (13), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 13
[2025-04-28 21:22:00,055 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,056 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:22:00,057 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:22:00,057 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 21 SyntacticMatches, 1 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 11 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=100, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:22:00,058 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 5 mSDsluCounter, 57 mSDsCounter, 0 mSdLazyCounter, 98 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 72 SdHoareTripleChecker+Invalid, 105 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 98 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,058 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 72 Invalid, 105 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 98 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:00,059 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:22:00,065 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 19.
[2025-04-28 21:22:00,066 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 19 states, 8 states have (on average 1.375) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 2 states have call predecessors, (5), 5 states have return successors, (14), 5 states have call predecessors, (14), 5 states have call successors, (14)
[2025-04-28 21:22:00,066 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 19 states to 19 states and 30 transitions.
[2025-04-28 21:22:00,067 INFO  L79                 Accepts]: Start accepts. Automaton has 19 states and 30 transitions. Word has length 13
[2025-04-28 21:22:00,067 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,067 INFO  L485      AbstractCegarLoop]: Abstraction has 19 states and 30 transitions.
[2025-04-28 21:22:00,067 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 10 states have internal predecessors, (13), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:22:00,067 INFO  L278                IsEmpty]: Start isEmpty. Operand 19 states and 30 transitions.
[2025-04-28 21:22:00,068 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:22:00,068 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,068 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,074 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:00,269 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,269 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,270 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,270 INFO  L85        PathProgramCache]: Analyzing trace with hash -58935186, now seen corresponding path program 1 times
[2025-04-28 21:22:00,270 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,270 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [85720024]
[2025-04-28 21:22:00,270 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,270 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,279 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:22:00,286 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:00,287 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,287 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,371 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:00,371 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,371 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [85720024]
[2025-04-28 21:22:00,371 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [85720024] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:00,371 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:00,371 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:00,371 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2135248739]
[2025-04-28 21:22:00,371 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,372 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:00,372 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,373 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:00,373 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:00,373 INFO  L87              Difference]: Start difference. First operand 19 states and 30 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:00,486 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,486 INFO  L93              Difference]: Finished difference Result 36 states and 63 transitions.
[2025-04-28 21:22:00,487 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:00,488 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:22:00,488 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,489 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:22:00,491 INFO  L226             Difference]: Without dead ends: 36
[2025-04-28 21:22:00,492 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:00,492 INFO  L437           NwaCegarLoop]: 21 mSDtfsCounter, 5 mSDsluCounter, 16 mSDsCounter, 0 mSdLazyCounter, 48 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 37 SdHoareTripleChecker+Invalid, 51 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 48 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,495 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 37 Invalid, 51 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 48 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:00,496 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 36 states.
[2025-04-28 21:22:00,509 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 36 to 28.
[2025-04-28 21:22:00,511 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 12 states have (on average 1.5) internal successors, (18), 17 states have internal predecessors, (18), 7 states have call successors, (7), 3 states have call predecessors, (7), 8 states have return successors, (23), 7 states have call predecessors, (23), 7 states have call successors, (23)
[2025-04-28 21:22:00,513 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 48 transitions.
[2025-04-28 21:22:00,513 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 48 transitions. Word has length 17
[2025-04-28 21:22:00,513 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,513 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 48 transitions.
[2025-04-28 21:22:00,514 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:00,514 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 48 transitions.
[2025-04-28 21:22:00,515 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:22:00,515 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,515 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,515 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:22:00,516 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,516 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,516 INFO  L85        PathProgramCache]: Analyzing trace with hash -1296561645, now seen corresponding path program 2 times
[2025-04-28 21:22:00,517 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,517 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [118115636]
[2025-04-28 21:22:00,517 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:00,517 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,527 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:22:00,535 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:00,538 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:00,538 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,779 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:00,779 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,779 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [118115636]
[2025-04-28 21:22:00,780 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [118115636] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,780 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [429215546]
[2025-04-28 21:22:00,781 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:00,782 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,785 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,787 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:00,793 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,840 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:22:00,859 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:00,859 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:00,859 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,864 INFO  L256         TraceCheckSpWp]: Trace formula consists of 81 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,866 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:01,006 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:01,006 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:02,635 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:02,635 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [429215546] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:02,635 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:02,635 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 17
[2025-04-28 21:22:02,635 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [210563590]
[2025-04-28 21:22:02,636 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:02,636 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:22:02,636 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:02,637 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:22:02,637 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=48, Invalid=224, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:22:02,638 INFO  L87              Difference]: Start difference. First operand 28 states and 48 transitions. Second operand  has 17 states, 10 states have (on average 2.0) internal successors, (20), 16 states have internal predecessors, (20), 8 states have call successors, (8), 1 states have call predecessors, (8), 9 states have return successors, (10), 6 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:22:03,032 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,033 INFO  L93              Difference]: Finished difference Result 40 states and 72 transitions.
[2025-04-28 21:22:03,033 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:22:03,033 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 10 states have (on average 2.0) internal successors, (20), 16 states have internal predecessors, (20), 8 states have call successors, (8), 1 states have call predecessors, (8), 9 states have return successors, (10), 6 states have call predecessors, (10), 8 states have call successors, (10) Word has length 17
[2025-04-28 21:22:03,034 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,035 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:22:03,035 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:22:03,036 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 47 GetRequests, 25 SyntacticMatches, 1 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 61 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=110, Invalid=396, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:22:03,037 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 12 mSDsluCounter, 71 mSDsCounter, 0 mSdLazyCounter, 162 mSolverCounterSat, 39 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 87 SdHoareTripleChecker+Invalid, 201 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 39 IncrementalHoareTripleChecker+Valid, 162 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,037 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 87 Invalid, 201 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [39 Valid, 162 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:03,038 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:22:03,049 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 28.
[2025-04-28 21:22:03,049 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 12 states have (on average 1.5) internal successors, (18), 17 states have internal predecessors, (18), 7 states have call successors, (7), 3 states have call predecessors, (7), 8 states have return successors, (23), 7 states have call predecessors, (23), 7 states have call successors, (23)
[2025-04-28 21:22:03,050 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 48 transitions.
[2025-04-28 21:22:03,050 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 48 transitions. Word has length 17
[2025-04-28 21:22:03,050 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,051 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 48 transitions.
[2025-04-28 21:22:03,051 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 10 states have (on average 2.0) internal successors, (20), 16 states have internal predecessors, (20), 8 states have call successors, (8), 1 states have call predecessors, (8), 9 states have return successors, (10), 6 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:22:03,051 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 48 transitions.
[2025-04-28 21:22:03,052 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:22:03,053 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,053 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,057 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:03,253 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:03,253 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,254 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,254 INFO  L85        PathProgramCache]: Analyzing trace with hash 167574023, now seen corresponding path program 1 times
[2025-04-28 21:22:03,254 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,254 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [942496289]
[2025-04-28 21:22:03,254 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:03,255 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,260 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:22:03,266 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:03,266 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,266 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,318 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:03,318 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,318 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [942496289]
[2025-04-28 21:22:03,319 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [942496289] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:03,319 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:03,319 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:03,319 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [471954004]
[2025-04-28 21:22:03,319 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,319 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:03,319 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,320 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:03,320 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:03,320 INFO  L87              Difference]: Start difference. First operand 28 states and 48 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:03,409 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,409 INFO  L93              Difference]: Finished difference Result 36 states and 59 transitions.
[2025-04-28 21:22:03,410 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:03,410 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:22:03,411 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,411 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:22:03,411 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:22:03,412 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:03,412 INFO  L437           NwaCegarLoop]: 21 mSDtfsCounter, 5 mSDsluCounter, 16 mSDsCounter, 0 mSdLazyCounter, 42 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 37 SdHoareTripleChecker+Invalid, 45 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 42 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,413 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 37 Invalid, 45 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 42 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:03,413 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:22:03,424 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 24.
[2025-04-28 21:22:03,425 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 10 states have (on average 1.5) internal successors, (15), 14 states have internal predecessors, (15), 7 states have call successors, (7), 3 states have call predecessors, (7), 6 states have return successors, (17), 6 states have call predecessors, (17), 7 states have call successors, (17)
[2025-04-28 21:22:03,426 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 39 transitions.
[2025-04-28 21:22:03,426 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 39 transitions. Word has length 17
[2025-04-28 21:22:03,426 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,426 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 39 transitions.
[2025-04-28 21:22:03,426 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:03,426 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 39 transitions.
[2025-04-28 21:22:03,427 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:22:03,427 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,427 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,427 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:22:03,427 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,428 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,428 INFO  L85        PathProgramCache]: Analyzing trace with hash 704705570, now seen corresponding path program 1 times
[2025-04-28 21:22:03,428 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,428 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [412663456]
[2025-04-28 21:22:03,428 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:03,428 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,435 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:22:03,443 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:03,443 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,443 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,479 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:03,479 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,479 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [412663456]
[2025-04-28 21:22:03,479 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [412663456] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:03,479 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:03,479 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:03,479 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [842861839]
[2025-04-28 21:22:03,480 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,480 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:03,480 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,480 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:03,481 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:03,481 INFO  L87              Difference]: Start difference. First operand 24 states and 39 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:03,559 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,559 INFO  L93              Difference]: Finished difference Result 41 states and 62 transitions.
[2025-04-28 21:22:03,560 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:03,560 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:22:03,560 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,561 INFO  L225             Difference]: With dead ends: 41
[2025-04-28 21:22:03,561 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:22:03,561 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:22:03,562 INFO  L437           NwaCegarLoop]: 21 mSDtfsCounter, 4 mSDsluCounter, 14 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 35 SdHoareTripleChecker+Invalid, 44 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,562 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 35 Invalid, 44 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:03,563 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:22:03,567 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:22:03,568 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 13 states have (on average 1.3846153846153846) internal successors, (18), 16 states have internal predecessors, (18), 7 states have call successors, (7), 4 states have call predecessors, (7), 8 states have return successors, (16), 8 states have call predecessors, (16), 7 states have call successors, (16)
[2025-04-28 21:22:03,569 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 41 transitions.
[2025-04-28 21:22:03,569 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 41 transitions. Word has length 17
[2025-04-28 21:22:03,569 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,569 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 41 transitions.
[2025-04-28 21:22:03,569 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:22:03,569 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 41 transitions.
[2025-04-28 21:22:03,574 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:22:03,574 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,574 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,574 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:22:03,575 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,575 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,575 INFO  L85        PathProgramCache]: Analyzing trace with hash 1500002555, now seen corresponding path program 2 times
[2025-04-28 21:22:03,575 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,575 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [780023123]
[2025-04-28 21:22:03,575 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:03,575 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,579 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:22:03,588 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:03,588 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:03,588 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,776 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 5 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:03,776 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,776 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [780023123]
[2025-04-28 21:22:03,776 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [780023123] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:03,777 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1985307869]
[2025-04-28 21:22:03,777 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:03,777 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:03,780 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:03,782 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:03,785 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:22:03,837 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:22:03,853 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:03,853 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:03,853 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,854 INFO  L256         TraceCheckSpWp]: Trace formula consists of 89 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:03,856 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:04,018 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:04,020 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:05,411 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:05,411 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1985307869] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:05,411 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:05,412 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 15
[2025-04-28 21:22:05,412 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [5789666]
[2025-04-28 21:22:05,412 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,413 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:22:05,413 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,413 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:22:05,414 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=35, Invalid=175, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:22:05,414 INFO  L87              Difference]: Start difference. First operand 29 states and 41 transitions. Second operand  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (10), 5 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:22:05,666 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:05,666 INFO  L93              Difference]: Finished difference Result 39 states and 51 transitions.
[2025-04-28 21:22:05,666 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:05,666 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (10), 5 states have call predecessors, (10), 9 states have call successors, (10) Word has length 17
[2025-04-28 21:22:05,667 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:05,667 INFO  L225             Difference]: With dead ends: 39
[2025-04-28 21:22:05,667 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:22:05,668 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 46 GetRequests, 27 SyntacticMatches, 1 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 30 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=84, Invalid=296, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:22:05,669 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 15 mSDsluCounter, 90 mSDsCounter, 0 mSdLazyCounter, 108 mSolverCounterSat, 27 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 107 SdHoareTripleChecker+Invalid, 135 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 27 IncrementalHoareTripleChecker+Valid, 108 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:05,669 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 107 Invalid, 135 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [27 Valid, 108 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:05,669 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:22:05,673 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 18.
[2025-04-28 21:22:05,673 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 18 states, 8 states have (on average 1.375) internal successors, (11), 10 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 4 states have return successors, (6), 5 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:22:05,673 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 18 states to 18 states and 22 transitions.
[2025-04-28 21:22:05,674 INFO  L79                 Accepts]: Start accepts. Automaton has 18 states and 22 transitions. Word has length 17
[2025-04-28 21:22:05,674 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:05,674 INFO  L485      AbstractCegarLoop]: Abstraction has 18 states and 22 transitions.
[2025-04-28 21:22:05,674 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (10), 5 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:22:05,674 INFO  L278                IsEmpty]: Start isEmpty. Operand 18 states and 22 transitions.
[2025-04-28 21:22:05,675 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:22:05,675 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:05,675 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:05,681 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:22:05,879 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:05,879 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:05,880 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:05,880 INFO  L85        PathProgramCache]: Analyzing trace with hash 35866887, now seen corresponding path program 2 times
[2025-04-28 21:22:05,880 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:05,880 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2074606465]
[2025-04-28 21:22:05,880 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:05,880 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:05,884 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:22:05,892 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:05,893 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:05,893 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,287 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:06,287 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,288 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2074606465]
[2025-04-28 21:22:06,288 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2074606465] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:06,288 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [67074875]
[2025-04-28 21:22:06,288 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:06,288 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,291 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:06,293 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:06,298 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:22:06,358 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:22:06,374 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:06,374 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:06,374 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,376 WARN  L254         TraceCheckSpWp]: Trace formula consists of 85 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:06,378 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:06,635 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:06,636 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:08,143 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:08,144 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [67074875] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,144 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,146 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 18
[2025-04-28 21:22:08,150 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [647722156]
[2025-04-28 21:22:08,150 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,150 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:22:08,150 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,151 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:22:08,151 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=48, Invalid=258, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:22:08,152 INFO  L87              Difference]: Start difference. First operand 18 states and 22 transitions. Second operand  has 18 states, 10 states have (on average 2.0) internal successors, (20), 17 states have internal predecessors, (20), 9 states have call successors, (9), 1 states have call predecessors, (9), 9 states have return successors, (10), 7 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:22:08,834 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:08,834 INFO  L93              Difference]: Finished difference Result 37 states and 51 transitions.
[2025-04-28 21:22:08,834 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:08,835 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 10 states have (on average 2.0) internal successors, (20), 17 states have internal predecessors, (20), 9 states have call successors, (9), 1 states have call predecessors, (9), 9 states have return successors, (10), 7 states have call predecessors, (10), 9 states have call successors, (10) Word has length 17
[2025-04-28 21:22:08,835 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,835 INFO  L225             Difference]: With dead ends: 37
[2025-04-28 21:22:08,836 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:22:08,836 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 25 SyntacticMatches, 0 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 57 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=129, Invalid=521, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:22:08,837 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 17 mSDsluCounter, 108 mSDsCounter, 0 mSdLazyCounter, 183 mSolverCounterSat, 31 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 123 SdHoareTripleChecker+Invalid, 214 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 31 IncrementalHoareTripleChecker+Valid, 183 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,837 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 123 Invalid, 214 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [31 Valid, 183 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:08,838 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:22:08,844 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 24.
[2025-04-28 21:22:08,844 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 6 states have call successors, (6), 4 states have call predecessors, (6), 6 states have return successors, (9), 6 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:22:08,845 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 30 transitions.
[2025-04-28 21:22:08,845 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 30 transitions. Word has length 17
[2025-04-28 21:22:08,846 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,846 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 30 transitions.
[2025-04-28 21:22:08,846 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 10 states have (on average 2.0) internal successors, (20), 17 states have internal predecessors, (20), 9 states have call successors, (9), 1 states have call predecessors, (9), 9 states have return successors, (10), 7 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:22:08,846 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 30 transitions.
[2025-04-28 21:22:08,847 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:22:08,850 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,850 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:08,855 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:22:09,050 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,051 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,051 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,051 INFO  L85        PathProgramCache]: Analyzing trace with hash -1067520683, now seen corresponding path program 3 times
[2025-04-28 21:22:09,051 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,051 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1341110038]
[2025-04-28 21:22:09,051 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:09,051 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,056 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:22:09,062 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 19 of 21 statements.
[2025-04-28 21:22:09,062 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:22:09,063 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,265 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 6 proven. 5 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:22:09,265 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:09,265 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1341110038]
[2025-04-28 21:22:09,265 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1341110038] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:09,265 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [26652987]
[2025-04-28 21:22:09,265 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:09,265 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,268 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:09,271 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:09,274 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:09,333 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:22:09,351 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 19 of 21 statements.
[2025-04-28 21:22:09,351 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:22:09,352 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,353 INFO  L256         TraceCheckSpWp]: Trace formula consists of 105 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:09,355 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:09,572 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 2 proven. 11 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:09,572 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:12,089 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 6 proven. 7 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:12,090 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [26652987] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:12,090 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:12,090 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 10, 10] total 20
[2025-04-28 21:22:12,090 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1927039240]
[2025-04-28 21:22:12,090 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,090 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:22:12,091 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,091 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:22:12,092 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=317, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:22:12,092 INFO  L87              Difference]: Start difference. First operand 24 states and 30 transitions. Second operand  has 20 states, 10 states have (on average 2.4) internal successors, (24), 20 states have internal predecessors, (24), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (13), 8 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:22:12,320 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,320 INFO  L93              Difference]: Finished difference Result 30 states and 35 transitions.
[2025-04-28 21:22:12,321 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:22:12,321 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.4) internal successors, (24), 20 states have internal predecessors, (24), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (13), 8 states have call predecessors, (13), 11 states have call successors, (13) Word has length 21
[2025-04-28 21:22:12,322 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,322 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:22:12,322 INFO  L226             Difference]: Without dead ends: 23
[2025-04-28 21:22:12,323 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 31 SyntacticMatches, 0 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 70 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=134, Invalid=568, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:12,323 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 17 mSDsluCounter, 74 mSDsCounter, 0 mSdLazyCounter, 78 mSolverCounterSat, 23 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 88 SdHoareTripleChecker+Invalid, 101 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 23 IncrementalHoareTripleChecker+Valid, 78 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,324 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 88 Invalid, 101 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [23 Valid, 78 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:12,324 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 23 states.
[2025-04-28 21:22:12,326 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 23 to 21.
[2025-04-28 21:22:12,327 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 21 states, 10 states have (on average 1.2) internal successors, (12), 11 states have internal predecessors, (12), 5 states have call successors, (5), 4 states have call predecessors, (5), 5 states have return successors, (6), 5 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:22:12,327 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 21 states to 21 states and 23 transitions.
[2025-04-28 21:22:12,327 INFO  L79                 Accepts]: Start accepts. Automaton has 21 states and 23 transitions. Word has length 21
[2025-04-28 21:22:12,328 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:12,328 INFO  L485      AbstractCegarLoop]: Abstraction has 21 states and 23 transitions.
[2025-04-28 21:22:12,328 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.4) internal successors, (24), 20 states have internal predecessors, (24), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (13), 8 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:22:12,328 INFO  L278                IsEmpty]: Start isEmpty. Operand 21 states and 23 transitions.
[2025-04-28 21:22:12,329 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:22:12,329 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:12,329 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:12,336 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:22:12,533 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-04-28 21:22:12,533 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:12,534 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:12,534 INFO  L85        PathProgramCache]: Analyzing trace with hash 1512550473, now seen corresponding path program 4 times
[2025-04-28 21:22:12,534 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:12,534 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1709789183]
[2025-04-28 21:22:12,534 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:12,534 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:12,539 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:22:12,547 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:12,547 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:22:12,547 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:12,904 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 13 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:12,905 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:12,905 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1709789183]
[2025-04-28 21:22:12,905 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1709789183] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:12,905 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [978845305]
[2025-04-28 21:22:12,905 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:12,905 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:12,908 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:12,910 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:12,913 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:22:12,992 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:22:13,010 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:13,010 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:22:13,010 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,012 INFO  L256         TraceCheckSpWp]: Trace formula consists of 111 conjuncts, 51 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:13,014 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:13,279 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 1 proven. 12 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:13,279 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:14,539 INFO  L134       CoverageAnalysis]: Checked inductivity of 19 backedges. 0 proven. 13 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:22:14,539 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [978845305] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:14,539 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:14,540 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 22
[2025-04-28 21:22:14,540 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1668187896]
[2025-04-28 21:22:14,540 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:14,540 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:14,540 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:14,541 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:14,541 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=399, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:14,541 INFO  L87              Difference]: Start difference. First operand 21 states and 23 transitions. Second operand  has 22 states, 10 states have (on average 2.4) internal successors, (24), 21 states have internal predecessors, (24), 13 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (13), 7 states have call predecessors, (13), 13 states have call successors, (13)
[2025-04-28 21:22:15,211 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:15,211 INFO  L93              Difference]: Finished difference Result 27 states and 29 transitions.
[2025-04-28 21:22:15,211 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:22:15,212 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 10 states have (on average 2.4) internal successors, (24), 21 states have internal predecessors, (24), 13 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (13), 7 states have call predecessors, (13), 13 states have call successors, (13) Word has length 21
[2025-04-28 21:22:15,212 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:15,212 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:22:15,212 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:22:15,212 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 61 GetRequests, 31 SyntacticMatches, 0 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 98 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=190, Invalid=802, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:22:15,213 INFO  L437           NwaCegarLoop]: 13 mSDtfsCounter, 28 mSDsluCounter, 72 mSDsCounter, 0 mSdLazyCounter, 125 mSolverCounterSat, 69 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 30 SdHoareTripleChecker+Valid, 85 SdHoareTripleChecker+Invalid, 194 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 69 IncrementalHoareTripleChecker+Valid, 125 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:15,213 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [30 Valid, 85 Invalid, 194 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [69 Valid, 125 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:15,213 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:22:15,214 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:22:15,214 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:22:15,214 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:22:15,214 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 21
[2025-04-28 21:22:15,214 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:15,214 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:22:15,214 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 10 states have (on average 2.4) internal successors, (24), 21 states have internal predecessors, (24), 13 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (13), 7 states have call predecessors, (13), 13 states have call successors, (13)
[2025-04-28 21:22:15,214 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:22:15,214 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:22:15,217 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:22:15,221 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:15,418 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:22:15,421 INFO  L422         BasicCegarLoop]: Path program histogram: [4, 2, 2, 1, 1, 1, 1]
[2025-04-28 21:22:15,423 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:22:15,427 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:22:15 BoogieIcfgContainer
[2025-04-28 21:22:15,427 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:22:15,428 INFO  L158              Benchmark]: Toolchain (without parser) took 21097.17ms. Allocated memory was 234.9MB in the beginning and 268.4MB in the end (delta: 33.6MB). Free memory was 161.8MB in the beginning and 184.1MB in the end (delta: -22.3MB). Peak memory consumption was 26.6MB. Max. memory is 33.6GB.
[2025-04-28 21:22:15,428 INFO  L158              Benchmark]: SmtParser took 0.44ms. Allocated memory is still 234.9MB. Free memory was 171.5MB in the beginning and 170.9MB in the end (delta: 587.2kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:15,429 INFO  L158              Benchmark]: ChcToBoogie took 35.59ms. Allocated memory is still 234.9MB. Free memory was 161.8MB in the beginning and 161.2MB in the end (delta: 594.6kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:15,429 INFO  L158              Benchmark]: Boogie Preprocessor took 81.06ms. Allocated memory is still 234.9MB. Free memory was 161.2MB in the beginning and 158.7MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:22:15,429 INFO  L158              Benchmark]: RCFGBuilder took 301.01ms. Allocated memory is still 234.9MB. Free memory was 158.7MB in the beginning and 150.7MB in the end (delta: 8.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:22:15,430 INFO  L158              Benchmark]: TraceAbstraction took 20669.10ms. Allocated memory was 234.9MB in the beginning and 268.4MB in the end (delta: 33.6MB). Free memory was 150.1MB in the beginning and 184.1MB in the end (delta: -34.0MB). Peak memory consumption was 9.8MB. Max. memory is 33.6GB.
[2025-04-28 21:22:15,431 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.44ms. Allocated memory is still 234.9MB. Free memory was 171.5MB in the beginning and 170.9MB in the end (delta: 587.2kB). There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 35.59ms. Allocated memory is still 234.9MB. Free memory was 161.8MB in the beginning and 161.2MB in the end (delta: 594.6kB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 81.06ms. Allocated memory is still 234.9MB. Free memory was 161.2MB in the beginning and 158.7MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 301.01ms. Allocated memory is still 234.9MB. Free memory was 158.7MB in the beginning and 150.7MB in the end (delta: 8.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 20669.10ms. Allocated memory was 234.9MB in the beginning and 268.4MB in the end (delta: 33.6MB). Free memory was 150.1MB in the beginning and 184.1MB in the end (delta: -34.0MB). Peak memory consumption was 9.8MB. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 3 procedures, 15 locations, 25 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 20.6s, OverallIterations: 12, TraceHistogramMax: 4, PathProgramHistogramMax: 4, EmptinessCheckTime: 0.0s, AutomataDifference: 3.2s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 154 SdHoareTripleChecker+Valid, 1.6s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 116 mSDsluCounter, 795 SdHoareTripleChecker+Invalid, 1.4s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 595 mSDsCounter, 222 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 1013 IncrementalHoareTripleChecker+Invalid, 1235 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 222 mSolverCounterUnsat, 200 mSDtfsCounter, 1013 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 376 GetRequests, 214 SyntacticMatches, 4 SemanticMatches, 158 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 350 ImplicationChecksByTransitivity, 3.5s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=29occurred in iteration=8, InterpolantAutomatonStates: 97, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 12 MinimizatonAttempts, 62 StatesRemovedByMinimization, 8 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.1s SsaConstructionTime, 0.3s SatisfiabilityAnalysisTime, 14.5s InterpolantComputationTime, 324 NumberOfCodeBlocks, 320 NumberOfCodeBlocksAsserted, 30 NumberOfCheckSat, 428 ConstructedInterpolants, 0 QuantifiedInterpolants, 2536 SizeOfPredicates, 92 NumberOfNonLiveVariables, 652 ConjunctsInSsa, 196 ConjunctsInUnsatCore, 28 InterpolantComputations, 5 PerfectInterpolantSequences, 130/255 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:22:15,449 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
sat
