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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:47,586 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:47,694 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2efcc7dd-6224-4655-b4e0-cb55febc0356/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:47,700 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:47,701 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:47,740 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:47,742 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:47,742 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:47,743 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:47,743 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:47,743 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:47,743 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:47,743 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:47,743 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:47,744 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:47,744 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:47,744 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:47,744 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:47,744 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:47,744 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:47,744 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:47,745 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:47,745 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:47,745 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:47,746 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:47,748 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:47,748 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:48,104 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:48,112 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:48,115 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:48,117 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:48,117 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:48,119 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2efcc7dd-6224-4655-b4e0-cb55febc0356/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-181.smt2
[2025-04-28 21:21:48,120 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:48,124 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:48,313 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2efcc7dd-6224-4655-b4e0-cb55febc0356/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-181.smt2
[2025-04-28 21:21:48,317 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:48,318 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:48,319 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:48,320 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:48,320 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:48,323 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,354 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48 Unit
[2025-04-28 21:21:48,354 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:48,356 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:48,356 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:48,356 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:48,379 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,379 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,414 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,414 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,417 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,420 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,423 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,424 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,425 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,446 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:48,447 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:48,447 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:48,447 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:48,448 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (1/1) ...
[2025-04-28 21:21:48,452 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:48,469 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,486 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:48,494 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:48,507 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:48,507 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:48,507 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:48,507 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main26 given in one single declaration
[2025-04-28 21:21:48,508 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main26
[2025-04-28 21:21:48,508 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main26
[2025-04-28 21:21:48,508 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main22 given in one single declaration
[2025-04-28 21:21:48,508 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main22
[2025-04-28 21:21:48,508 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main22
[2025-04-28 21:21:48,508 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main13 given in one single declaration
[2025-04-28 21:21:48,508 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main13
[2025-04-28 21:21:48,508 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main13
[2025-04-28 21:21:48,508 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main8 given in one single declaration
[2025-04-28 21:21:48,508 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main8
[2025-04-28 21:21:48,508 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main8
[2025-04-28 21:21:48,509 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main3 given in one single declaration
[2025-04-28 21:21:48,509 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main3
[2025-04-28 21:21:48,509 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main3
[2025-04-28 21:21:48,509 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:48,509 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:48,509 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:48,572 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:48,575 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:48,715 INFO  L?                        ?]: Removed 1 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:48,715 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:48,731 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:48,731 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:48,732 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:48 BoogieIcfgContainer
[2025-04-28 21:21:48,732 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:48,739 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:48,739 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:48,743 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:48,743 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:48" (1/3) ...
[2025-04-28 21:21:48,744 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@18a89b01 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:48, skipping insertion in model container
[2025-04-28 21:21:48,744 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:48" (2/3) ...
[2025-04-28 21:21:48,744 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@18a89b01 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:48, skipping insertion in model container
[2025-04-28 21:21:48,745 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:48" (3/3) ...
[2025-04-28 21:21:48,746 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:48,762 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:48,764 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 30 locations, 44 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:48,810 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:48,823 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;@35fb8a9e, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:48,824 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:48,828 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 30 states, 13 states have (on average 1.3076923076923077) internal successors, (17), 17 states have internal predecessors, (17), 9 states have call successors, (9), 6 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 9 states have call successors, (9)
[2025-04-28 21:21:48,836 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:48,836 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,837 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,838 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,843 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,844 INFO  L85        PathProgramCache]: Analyzing trace with hash 1195751647, now seen corresponding path program 1 times
[2025-04-28 21:21:48,852 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,853 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [505454336]
[2025-04-28 21:21:48,853 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,854 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,889 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:48,911 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:48,912 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,912 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,206 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:49,207 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,207 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [505454336]
[2025-04-28 21:21:49,208 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [505454336] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,208 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,211 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:49,214 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1007330926]
[2025-04-28 21:21:49,216 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,220 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:49,220 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,250 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:49,250 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:49,253 INFO  L87              Difference]: Start difference. First operand  has 30 states, 13 states have (on average 1.3076923076923077) internal successors, (17), 17 states have internal predecessors, (17), 9 states have call successors, (9), 6 states have call predecessors, (9), 6 states have return successors, (9), 6 states have call predecessors, (9), 9 states have call successors, (9) Second operand  has 7 states, 5 states have (on average 2.4) internal successors, (12), 7 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 5 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:49,401 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,402 INFO  L93              Difference]: Finished difference Result 36 states and 43 transitions.
[2025-04-28 21:21:49,403 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:49,405 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.4) internal successors, (12), 7 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 5 states have call predecessors, (6), 4 states have call successors, (6) Word has length 24
[2025-04-28 21:21:49,405 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,412 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:49,413 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:49,415 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:49,418 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 3 mSDsluCounter, 128 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 157 SdHoareTripleChecker+Invalid, 34 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 34 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,419 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 157 Invalid, 34 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 34 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:49,435 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:49,477 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 32.
[2025-04-28 21:21:49,478 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 14 states have (on average 1.2142857142857142) internal successors, (17), 17 states have internal predecessors, (17), 9 states have call successors, (9), 6 states have call predecessors, (9), 8 states have return successors, (12), 8 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:49,482 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 38 transitions.
[2025-04-28 21:21:49,484 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 38 transitions. Word has length 24
[2025-04-28 21:21:49,484 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,484 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 38 transitions.
[2025-04-28 21:21:49,484 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.4) internal successors, (12), 7 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 5 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:49,485 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 38 transitions.
[2025-04-28 21:21:49,486 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:49,486 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,486 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,487 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:49,487 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,488 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,488 INFO  L85        PathProgramCache]: Analyzing trace with hash 38167296, now seen corresponding path program 1 times
[2025-04-28 21:21:49,488 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,488 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [545386468]
[2025-04-28 21:21:49,488 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,489 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,501 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:49,511 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:49,512 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,512 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,910 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:49,910 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,910 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [545386468]
[2025-04-28 21:21:49,911 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [545386468] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:49,911 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [226889790]
[2025-04-28 21:21:49,911 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,911 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,915 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,920 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:49,922 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,980 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:50,025 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:50,025 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,028 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,033 INFO  L256         TraceCheckSpWp]: Trace formula consists of 99 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,047 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,292 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:50,293 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,875 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:51,875 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [226889790] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:51,875 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:51,875 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [10, 10] total 20
[2025-04-28 21:21:51,876 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1257216744]
[2025-04-28 21:21:51,876 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,877 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:51,877 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,878 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:51,878 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=317, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:51,878 INFO  L87              Difference]: Start difference. First operand 32 states and 38 transitions. Second operand  has 10 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 6 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:51,994 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,994 INFO  L93              Difference]: Finished difference Result 34 states and 40 transitions.
[2025-04-28 21:21:51,995 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:51,995 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 6 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 6 states have call successors, (7) Word has length 28
[2025-04-28 21:21:51,996 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,997 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:51,997 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:51,997 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 65 GetRequests, 43 SyntacticMatches, 4 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 62 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=63, Invalid=317, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:51,998 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 2 mSDsluCounter, 124 mSDsCounter, 0 mSdLazyCounter, 59 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 154 SdHoareTripleChecker+Invalid, 60 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 59 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,999 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 154 Invalid, 60 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 59 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:52,000 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:52,003 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 30.
[2025-04-28 21:21:52,004 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 30 states, 13 states have (on average 1.2307692307692308) internal successors, (16), 16 states have internal predecessors, (16), 9 states have call successors, (9), 6 states have call predecessors, (9), 7 states have return successors, (10), 7 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:21:52,005 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 35 transitions.
[2025-04-28 21:21:52,006 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 35 transitions. Word has length 28
[2025-04-28 21:21:52,006 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,006 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 35 transitions.
[2025-04-28 21:21:52,006 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 6 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:52,006 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 35 transitions.
[2025-04-28 21:21:52,007 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:52,007 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,008 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,012 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:52,209 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:52,209 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,209 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,210 INFO  L85        PathProgramCache]: Analyzing trace with hash 297122768, now seen corresponding path program 1 times
[2025-04-28 21:21:52,210 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,210 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [701561895]
[2025-04-28 21:21:52,210 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,210 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,220 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:52,226 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:52,226 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,226 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,469 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:52,470 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,470 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [701561895]
[2025-04-28 21:21:52,470 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [701561895] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,470 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,470 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:52,470 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [548856776]
[2025-04-28 21:21:52,470 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,470 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:52,471 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,471 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:52,471 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:52,471 INFO  L87              Difference]: Start difference. First operand 30 states and 35 transitions. Second operand  has 8 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:52,574 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,574 INFO  L93              Difference]: Finished difference Result 34 states and 39 transitions.
[2025-04-28 21:21:52,575 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:52,575 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 5 states have call successors, (7) Word has length 28
[2025-04-28 21:21:52,575 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,576 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:52,576 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:52,576 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:52,577 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 4 mSDsluCounter, 154 mSDsCounter, 0 mSdLazyCounter, 47 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 184 SdHoareTripleChecker+Invalid, 48 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 47 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,577 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 184 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 47 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:52,581 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:52,585 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:21:52,588 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 14 states have (on average 1.2142857142857142) internal successors, (17), 17 states have internal predecessors, (17), 9 states have call successors, (9), 6 states have call predecessors, (9), 8 states have return successors, (11), 8 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:52,588 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 37 transitions.
[2025-04-28 21:21:52,589 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 37 transitions. Word has length 28
[2025-04-28 21:21:52,589 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,589 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 37 transitions.
[2025-04-28 21:21:52,589 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 5 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:52,589 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 37 transitions.
[2025-04-28 21:21:52,590 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:52,590 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,590 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,590 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:52,593 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,594 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,594 INFO  L85        PathProgramCache]: Analyzing trace with hash -1784701263, now seen corresponding path program 1 times
[2025-04-28 21:21:52,594 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,594 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1506629887]
[2025-04-28 21:21:52,594 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,594 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,602 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:52,612 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:52,612 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,613 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,803 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:52,803 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,803 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1506629887]
[2025-04-28 21:21:52,803 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1506629887] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,803 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,803 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:52,803 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1027931983]
[2025-04-28 21:21:52,803 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,804 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:52,804 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,804 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:52,804 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:52,805 INFO  L87              Difference]: Start difference. First operand 32 states and 37 transitions. Second operand  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 4 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:52,881 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,881 INFO  L93              Difference]: Finished difference Result 40 states and 46 transitions.
[2025-04-28 21:21:52,881 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:52,882 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 4 states have call predecessors, (8), 5 states have call successors, (8) Word has length 32
[2025-04-28 21:21:52,882 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,883 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:21:52,883 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:52,883 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:52,884 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 5 mSDsluCounter, 161 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 191 SdHoareTripleChecker+Invalid, 43 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,884 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 191 Invalid, 43 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:52,885 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:52,889 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 34.
[2025-04-28 21:21:52,889 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 15 states have (on average 1.2) internal successors, (18), 18 states have internal predecessors, (18), 9 states have call successors, (9), 6 states have call predecessors, (9), 9 states have return successors, (12), 9 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:52,890 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 39 transitions.
[2025-04-28 21:21:52,890 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 39 transitions. Word has length 32
[2025-04-28 21:21:52,890 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,891 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 39 transitions.
[2025-04-28 21:21:52,891 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 4 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:52,891 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 39 transitions.
[2025-04-28 21:21:52,892 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:52,892 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,892 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,892 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:52,892 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,893 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,893 INFO  L85        PathProgramCache]: Analyzing trace with hash -231406613, now seen corresponding path program 1 times
[2025-04-28 21:21:52,893 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,893 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1846945460]
[2025-04-28 21:21:52,893 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,893 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,900 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:52,910 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:52,910 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,910 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,337 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:53,337 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,337 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1846945460]
[2025-04-28 21:21:53,337 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1846945460] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,337 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [876428766]
[2025-04-28 21:21:53,337 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,337 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,341 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,343 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:53,347 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,406 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:53,430 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:53,431 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,431 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,434 INFO  L256         TraceCheckSpWp]: Trace formula consists of 135 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,438 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,838 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:53,839 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,076 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:56,076 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [876428766] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,076 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,076 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 12, 12] total 28
[2025-04-28 21:21:56,077 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1787922957]
[2025-04-28 21:21:56,077 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,078 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 28 states
[2025-04-28 21:21:56,078 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,079 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 28 interpolants.
[2025-04-28 21:21:56,081 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=71, Invalid=685, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:56,081 INFO  L87              Difference]: Start difference. First operand 34 states and 39 transitions. Second operand  has 28 states, 14 states have (on average 2.5) internal successors, (35), 28 states have internal predecessors, (35), 17 states have call successors, (20), 1 states have call predecessors, (20), 14 states have return successors, (22), 14 states have call predecessors, (22), 17 states have call successors, (22)
[2025-04-28 21:21:56,458 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,458 INFO  L93              Difference]: Finished difference Result 42 states and 48 transitions.
[2025-04-28 21:21:56,459 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:56,459 INFO  L79                 Accepts]: Start accepts. Automaton has  has 28 states, 14 states have (on average 2.5) internal successors, (35), 28 states have internal predecessors, (35), 17 states have call successors, (20), 1 states have call predecessors, (20), 14 states have return successors, (22), 14 states have call predecessors, (22), 17 states have call successors, (22) Word has length 36
[2025-04-28 21:21:56,459 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,460 INFO  L225             Difference]: With dead ends: 42
[2025-04-28 21:21:56,460 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:21:56,461 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 91 GetRequests, 59 SyntacticMatches, 0 SemanticMatches, 32 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 112 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=110, Invalid=1012, Unknown=0, NotChecked=0, Total=1122
[2025-04-28 21:21:56,461 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 16 mSDsluCounter, 354 mSDsCounter, 0 mSdLazyCounter, 183 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 383 SdHoareTripleChecker+Invalid, 195 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 183 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,462 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 383 Invalid, 195 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 183 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:56,462 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:21:56,467 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 38.
[2025-04-28 21:21:56,467 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 38 states, 17 states have (on average 1.1764705882352942) internal successors, (20), 20 states have internal predecessors, (20), 9 states have call successors, (9), 6 states have call predecessors, (9), 11 states have return successors, (15), 11 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:21:56,468 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 38 states to 38 states and 44 transitions.
[2025-04-28 21:21:56,468 INFO  L79                 Accepts]: Start accepts. Automaton has 38 states and 44 transitions. Word has length 36
[2025-04-28 21:21:56,468 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,468 INFO  L485      AbstractCegarLoop]: Abstraction has 38 states and 44 transitions.
[2025-04-28 21:21:56,469 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 28 states, 14 states have (on average 2.5) internal successors, (35), 28 states have internal predecessors, (35), 17 states have call successors, (20), 1 states have call predecessors, (20), 14 states have return successors, (22), 14 states have call predecessors, (22), 17 states have call successors, (22)
[2025-04-28 21:21:56,469 INFO  L278                IsEmpty]: Start isEmpty. Operand 38 states and 44 transitions.
[2025-04-28 21:21:56,470 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:56,470 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,470 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,475 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:56,674 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,674 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,675 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,675 INFO  L85        PathProgramCache]: Analyzing trace with hash 1980108300, now seen corresponding path program 2 times
[2025-04-28 21:21:56,675 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,676 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2001740429]
[2025-04-28 21:21:56,676 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:56,676 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,688 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 40 statements into 2 equivalence classes.
[2025-04-28 21:21:56,698 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:56,699 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:56,699 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,009 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:57,009 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,010 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2001740429]
[2025-04-28 21:21:57,010 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2001740429] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,010 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1211092180]
[2025-04-28 21:21:57,010 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:57,010 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,013 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,015 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:57,019 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,075 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 40 statements into 2 equivalence classes.
[2025-04-28 21:21:57,105 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:57,105 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:57,105 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,106 INFO  L256         TraceCheckSpWp]: Trace formula consists of 152 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,108 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,271 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:57,271 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,301 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:01,302 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1211092180] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,302 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,302 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 14] total 27
[2025-04-28 21:22:01,302 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1154675412]
[2025-04-28 21:22:01,302 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,303 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:22:01,303 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,304 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:22:01,304 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=90, Invalid=612, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:01,304 INFO  L87              Difference]: Start difference. First operand 38 states and 44 transitions. Second operand  has 27 states, 13 states have (on average 2.6153846153846154) internal successors, (34), 27 states have internal predecessors, (34), 18 states have call successors, (20), 1 states have call predecessors, (20), 13 states have return successors, (22), 12 states have call predecessors, (22), 18 states have call successors, (22)
[2025-04-28 21:22:01,572 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,572 INFO  L93              Difference]: Finished difference Result 42 states and 48 transitions.
[2025-04-28 21:22:01,573 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:01,573 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 13 states have (on average 2.6153846153846154) internal successors, (34), 27 states have internal predecessors, (34), 18 states have call successors, (20), 1 states have call predecessors, (20), 13 states have return successors, (22), 12 states have call predecessors, (22), 18 states have call successors, (22) Word has length 40
[2025-04-28 21:22:01,573 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,574 INFO  L225             Difference]: With dead ends: 42
[2025-04-28 21:22:01,574 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:22:01,575 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 100 GetRequests, 64 SyntacticMatches, 5 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 195 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=147, Invalid=909, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:01,576 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 11 mSDsluCounter, 275 mSDsCounter, 0 mSdLazyCounter, 162 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 307 SdHoareTripleChecker+Invalid, 172 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 162 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,576 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 307 Invalid, 172 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 162 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:01,577 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:22:01,581 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 36.
[2025-04-28 21:22:01,581 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 16 states have (on average 1.1875) internal successors, (19), 19 states have internal predecessors, (19), 9 states have call successors, (9), 6 states have call predecessors, (9), 10 states have return successors, (13), 10 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:22:01,583 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 41 transitions.
[2025-04-28 21:22:01,584 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 41 transitions. Word has length 40
[2025-04-28 21:22:01,584 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,584 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 41 transitions.
[2025-04-28 21:22:01,584 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 13 states have (on average 2.6153846153846154) internal successors, (34), 27 states have internal predecessors, (34), 18 states have call successors, (20), 1 states have call predecessors, (20), 13 states have return successors, (22), 12 states have call predecessors, (22), 18 states have call successors, (22)
[2025-04-28 21:22:01,584 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 41 transitions.
[2025-04-28 21:22:01,587 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:22:01,588 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,588 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,593 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:22:01,791 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,791 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,792 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,792 INFO  L85        PathProgramCache]: Analyzing trace with hash 852273884, now seen corresponding path program 3 times
[2025-04-28 21:22:01,792 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,792 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [253988214]
[2025-04-28 21:22:01,792 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:01,792 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,798 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 40 statements into 3 equivalence classes.
[2025-04-28 21:22:01,809 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:22:01,809 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:22:01,809 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,001 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:02,001 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,001 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [253988214]
[2025-04-28 21:22:02,001 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [253988214] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,001 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1788504872]
[2025-04-28 21:22:02,001 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:02,001 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,004 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:02,006 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:02,010 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,111 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 40 statements into 3 equivalence classes.
[2025-04-28 21:22:02,134 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:22:02,135 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:22:02,135 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,137 INFO  L256         TraceCheckSpWp]: Trace formula consists of 154 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,139 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,319 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:02,320 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:05,399 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:05,400 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1788504872] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:05,400 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:05,400 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 23
[2025-04-28 21:22:05,400 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1022114150]
[2025-04-28 21:22:05,400 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,401 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:22:05,403 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,404 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:22:05,404 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=448, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:22:05,404 INFO  L87              Difference]: Start difference. First operand 36 states and 41 transitions. Second operand  has 23 states, 10 states have (on average 3.2) internal successors, (32), 23 states have internal predecessors, (32), 16 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (20), 9 states have call predecessors, (20), 16 states have call successors, (20)
[2025-04-28 21:22:05,796 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:05,796 INFO  L93              Difference]: Finished difference Result 50 states and 58 transitions.
[2025-04-28 21:22:05,798 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:22:05,798 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 10 states have (on average 3.2) internal successors, (32), 23 states have internal predecessors, (32), 16 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (20), 9 states have call predecessors, (20), 16 states have call successors, (20) Word has length 40
[2025-04-28 21:22:05,798 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:05,799 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:22:05,799 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:22:05,800 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 105 GetRequests, 64 SyntacticMatches, 7 SemanticMatches, 34 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 161 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=144, Invalid=1116, Unknown=0, NotChecked=0, Total=1260
[2025-04-28 21:22:05,801 INFO  L437           NwaCegarLoop]: 30 mSDtfsCounter, 21 mSDsluCounter, 328 mSDsCounter, 0 mSdLazyCounter, 192 mSolverCounterSat, 24 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 30 SdHoareTripleChecker+Valid, 358 SdHoareTripleChecker+Invalid, 216 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 24 IncrementalHoareTripleChecker+Valid, 192 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:05,801 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [30 Valid, 358 Invalid, 216 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [24 Valid, 192 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:05,802 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:22:05,806 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 40.
[2025-04-28 21:22:05,806 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 18 states have (on average 1.1666666666666667) internal successors, (21), 21 states have internal predecessors, (21), 9 states have call successors, (9), 6 states have call predecessors, (9), 12 states have return successors, (15), 12 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:22:05,807 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 45 transitions.
[2025-04-28 21:22:05,807 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 45 transitions. Word has length 40
[2025-04-28 21:22:05,812 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:05,812 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 45 transitions.
[2025-04-28 21:22:05,812 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 10 states have (on average 3.2) internal successors, (32), 23 states have internal predecessors, (32), 16 states have call successors, (20), 1 states have call predecessors, (20), 10 states have return successors, (20), 9 states have call predecessors, (20), 16 states have call successors, (20)
[2025-04-28 21:22:05,812 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 45 transitions.
[2025-04-28 21:22:05,813 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:22:05,813 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:05,813 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:05,823 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:06,014 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,014 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,015 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,015 INFO  L85        PathProgramCache]: Analyzing trace with hash -272251017, now seen corresponding path program 4 times
[2025-04-28 21:22:06,015 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,015 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1696886915]
[2025-04-28 21:22:06,015 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:06,015 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,024 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 48 statements into 2 equivalence classes.
[2025-04-28 21:22:06,033 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:22:06,033 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:22:06,033 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,483 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 0 proven. 12 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:22:06,483 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,484 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1696886915]
[2025-04-28 21:22:06,484 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1696886915] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:06,484 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1188364598]
[2025-04-28 21:22:06,484 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:06,484 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,486 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:06,488 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:06,492 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:22:06,616 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 48 statements into 2 equivalence classes.
[2025-04-28 21:22:06,648 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:22:06,648 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:22:06,648 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,651 INFO  L256         TraceCheckSpWp]: Trace formula consists of 188 conjuncts, 69 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:06,653 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:07,416 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 0 proven. 14 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:22:07,416 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:11,713 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 0 proven. 14 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:22:11,714 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1188364598] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:11,714 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:11,714 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 16, 16] total 36
[2025-04-28 21:22:11,714 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [932282498]
[2025-04-28 21:22:11,714 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:11,715 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 36 states
[2025-04-28 21:22:11,715 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:11,717 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 36 interpolants.
[2025-04-28 21:22:11,718 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=93, Invalid=1167, Unknown=0, NotChecked=0, Total=1260
[2025-04-28 21:22:11,718 INFO  L87              Difference]: Start difference. First operand 40 states and 45 transitions. Second operand  has 36 states, 18 states have (on average 2.388888888888889) internal successors, (43), 36 states have internal predecessors, (43), 21 states have call successors, (24), 1 states have call predecessors, (24), 18 states have return successors, (28), 18 states have call predecessors, (28), 21 states have call successors, (28)
[2025-04-28 21:22:12,540 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,540 INFO  L93              Difference]: Finished difference Result 50 states and 56 transitions.
[2025-04-28 21:22:12,541 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:22:12,541 INFO  L79                 Accepts]: Start accepts. Automaton has  has 36 states, 18 states have (on average 2.388888888888889) internal successors, (43), 36 states have internal predecessors, (43), 21 states have call successors, (24), 1 states have call predecessors, (24), 18 states have return successors, (28), 18 states have call predecessors, (28), 21 states have call successors, (28) Word has length 48
[2025-04-28 21:22:12,542 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,543 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:22:12,543 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:22:12,543 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 124 GetRequests, 77 SyntacticMatches, 3 SemanticMatches, 44 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 267 ImplicationChecksByTransitivity, 1.7s TimeCoverageRelationStatistics Valid=173, Invalid=1897, Unknown=0, NotChecked=0, Total=2070
[2025-04-28 21:22:12,544 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 32 mSDsluCounter, 575 mSDsCounter, 0 mSdLazyCounter, 314 mSolverCounterSat, 40 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 35 SdHoareTripleChecker+Valid, 606 SdHoareTripleChecker+Invalid, 354 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 40 IncrementalHoareTripleChecker+Valid, 314 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,545 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [35 Valid, 606 Invalid, 354 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [40 Valid, 314 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:22:12,545 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:22:12,550 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 44.
[2025-04-28 21:22:12,551 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 44 states, 20 states have (on average 1.15) internal successors, (23), 23 states have internal predecessors, (23), 9 states have call successors, (9), 6 states have call predecessors, (9), 14 states have return successors, (18), 14 states have call predecessors, (18), 9 states have call successors, (18)
[2025-04-28 21:22:12,552 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 44 states to 44 states and 50 transitions.
[2025-04-28 21:22:12,552 INFO  L79                 Accepts]: Start accepts. Automaton has 44 states and 50 transitions. Word has length 48
[2025-04-28 21:22:12,552 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:12,552 INFO  L485      AbstractCegarLoop]: Abstraction has 44 states and 50 transitions.
[2025-04-28 21:22:12,553 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 36 states, 18 states have (on average 2.388888888888889) internal successors, (43), 36 states have internal predecessors, (43), 21 states have call successors, (24), 1 states have call predecessors, (24), 18 states have return successors, (28), 18 states have call predecessors, (28), 21 states have call successors, (28)
[2025-04-28 21:22:12,553 INFO  L278                IsEmpty]: Start isEmpty. Operand 44 states and 50 transitions.
[2025-04-28 21:22:12,554 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:22:12,554 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:12,554 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:12,562 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:22:12,755 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:12,755 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:12,755 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:12,756 INFO  L85        PathProgramCache]: Analyzing trace with hash 561484184, now seen corresponding path program 5 times
[2025-04-28 21:22:12,756 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:12,756 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1503340380]
[2025-04-28 21:22:12,756 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:22:12,756 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:12,763 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 52 statements into 4 equivalence classes.
[2025-04-28 21:22:12,774 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:22:12,775 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s)
[2025-04-28 21:22:12,775 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,236 INFO  L134       CoverageAnalysis]: Checked inductivity of 41 backedges. 6 proven. 19 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:22:13,236 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,237 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1503340380]
[2025-04-28 21:22:13,237 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1503340380] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:13,237 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1947965492]
[2025-04-28 21:22:13,237 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:22:13,237 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,240 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:13,242 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:13,250 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:22:13,394 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 52 statements into 4 equivalence classes.
[2025-04-28 21:22:13,426 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:22:13,426 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s)
[2025-04-28 21:22:13,426 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,428 INFO  L256         TraceCheckSpWp]: Trace formula consists of 205 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:13,430 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:13,556 INFO  L134       CoverageAnalysis]: Checked inductivity of 41 backedges. 6 proven. 14 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:22:13,556 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
