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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:16,182 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:16,279 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_325da308-401f-487e-a607-5d56c5b3aeed/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:16,287 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:16,287 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:16,327 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:16,329 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:16,329 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:16,330 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:16,330 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:16,331 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:16,332 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:16,332 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:16,332 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:16,332 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:16,332 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:16,333 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:16,333 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:16,333 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:16,334 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:16,334 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:16,334 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:16,334 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:16,334 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:16,334 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:16,335 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:16,335 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:16,761 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:16,774 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:16,777 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:16,780 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:16,781 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:16,782 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_325da308-401f-487e-a607-5d56c5b3aeed/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-158.smt2
[2025-04-28 21:21:16,786 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:16,791 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:17,087 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_325da308-401f-487e-a607-5d56c5b3aeed/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-158.smt2
[2025-04-28 21:21:17,091 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:17,093 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:17,094 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:17,094 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:17,094 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:17,097 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,121 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17 Unit
[2025-04-28 21:21:17,122 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:17,123 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:17,123 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:17,123 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:17,142 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,142 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,176 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,178 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,180 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,183 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,186 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,189 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,192 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,205 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:17,206 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:17,206 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:17,206 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:17,208 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,211 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:17,230 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:17,247 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:17,252 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:17,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:17,266 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:17,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:17,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_2 given in one single declaration
[2025-04-28 21:21:17,266 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_2
[2025-04-28 21:21:17,266 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_2
[2025-04-28 21:21:17,266 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:17,267 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:17,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:17,267 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:17,267 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:17,267 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:17,322 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:17,326 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:17,528 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:17,530 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:17,548 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:17,549 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:17,550 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17 BoogieIcfgContainer
[2025-04-28 21:21:17,551 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:17,554 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:17,557 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:17,562 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:17,562 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:17" (1/3) ...
[2025-04-28 21:21:17,563 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4541562d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,564 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (2/3) ...
[2025-04-28 21:21:17,565 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4541562d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,565 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17" (3/3) ...
[2025-04-28 21:21:17,567 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:17,593 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:17,596 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 22 locations, 42 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:17,659 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:17,685 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;@7d783697, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:17,686 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:17,691 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 22 states, 8 states have (on average 1.875) internal successors, (15), 15 states have internal predecessors, (15), 9 states have call successors, (9), 3 states have call predecessors, (9), 3 states have return successors, (9), 4 states have call predecessors, (9), 9 states have call successors, (9)
[2025-04-28 21:21:17,702 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:17,702 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,703 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,704 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,710 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,711 INFO  L85        PathProgramCache]: Analyzing trace with hash -327235407, now seen corresponding path program 1 times
[2025-04-28 21:21:17,719 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,720 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1223253819]
[2025-04-28 21:21:17,720 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,720 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,758 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:17,785 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:17,786 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,786 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,958 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:17,959 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,959 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1223253819]
[2025-04-28 21:21:17,960 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1223253819] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,960 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,963 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:17,965 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [755111025]
[2025-04-28 21:21:17,966 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,970 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:17,970 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,996 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:17,997 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:17,999 INFO  L87              Difference]: Start difference. First operand  has 22 states, 8 states have (on average 1.875) internal successors, (15), 15 states have internal predecessors, (15), 9 states have call successors, (9), 3 states have call predecessors, (9), 3 states have return successors, (9), 4 states have call predecessors, (9), 9 states have call successors, (9) Second operand  has 5 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:18,151 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,152 INFO  L93              Difference]: Finished difference Result 24 states and 40 transitions.
[2025-04-28 21:21:18,154 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:18,155 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3) Word has length 13
[2025-04-28 21:21:18,156 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,164 INFO  L225             Difference]: With dead ends: 24
[2025-04-28 21:21:18,164 INFO  L226             Difference]: Without dead ends: 24
[2025-04-28 21:21:18,167 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:18,172 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 1 mSDsluCounter, 55 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 79 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,175 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 79 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:18,199 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 24 states.
[2025-04-28 21:21:18,235 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 24 to 24.
[2025-04-28 21:21:18,239 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 9 states have (on average 1.6666666666666667) internal successors, (15), 15 states have internal predecessors, (15), 9 states have call successors, (9), 3 states have call predecessors, (9), 5 states have return successors, (16), 5 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:18,247 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 40 transitions.
[2025-04-28 21:21:18,248 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 40 transitions. Word has length 13
[2025-04-28 21:21:18,251 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,251 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 40 transitions.
[2025-04-28 21:21:18,251 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:18,251 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 40 transitions.
[2025-04-28 21:21:18,254 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:18,254 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,255 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,255 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:18,255 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,258 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,258 INFO  L85        PathProgramCache]: Analyzing trace with hash 1473780768, now seen corresponding path program 1 times
[2025-04-28 21:21:18,258 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,259 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1663503429]
[2025-04-28 21:21:18,259 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,259 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,276 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:18,330 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:18,330 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,332 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,798 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:18,798 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,798 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1663503429]
[2025-04-28 21:21:18,798 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1663503429] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:18,798 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [290625090]
[2025-04-28 21:21:18,799 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,799 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:18,803 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:18,809 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:18,813 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:18,870 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:18,901 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:18,901 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,901 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,908 INFO  L256         TraceCheckSpWp]: Trace formula consists of 81 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:18,917 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:19,177 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:19,179 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:19,927 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:19,928 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [290625090] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:19,928 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:19,929 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 14
[2025-04-28 21:21:19,929 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1704348872]
[2025-04-28 21:21:19,930 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,932 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:19,932 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,933 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:19,934 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=140, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:19,935 INFO  L87              Difference]: Start difference. First operand 24 states and 40 transitions. Second operand  has 14 states, 7 states have (on average 2.142857142857143) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:20,433 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,434 INFO  L93              Difference]: Finished difference Result 46 states and 96 transitions.
[2025-04-28 21:21:20,434 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:20,435 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.142857142857143) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10) Word has length 17
[2025-04-28 21:21:20,435 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,437 INFO  L225             Difference]: With dead ends: 46
[2025-04-28 21:21:20,437 INFO  L226             Difference]: Without dead ends: 44
[2025-04-28 21:21:20,438 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 46 GetRequests, 29 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=85, Invalid=257, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:20,441 INFO  L437           NwaCegarLoop]: 20 mSDtfsCounter, 17 mSDsluCounter, 100 mSDsCounter, 0 mSdLazyCounter, 186 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 120 SdHoareTripleChecker+Invalid, 208 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 186 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,441 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 120 Invalid, 208 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 186 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:20,443 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 44 states.
[2025-04-28 21:21:20,457 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 44 to 32.
[2025-04-28 21:21:20,457 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 12 states have (on average 1.75) internal successors, (21), 20 states have internal predecessors, (21), 12 states have call successors, (12), 4 states have call predecessors, (12), 7 states have return successors, (28), 7 states have call predecessors, (28), 12 states have call successors, (28)
[2025-04-28 21:21:20,458 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 61 transitions.
[2025-04-28 21:21:20,459 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 61 transitions. Word has length 17
[2025-04-28 21:21:20,459 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,459 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 61 transitions.
[2025-04-28 21:21:20,459 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.142857142857143) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:20,459 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 61 transitions.
[2025-04-28 21:21:20,461 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:20,461 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,461 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,466 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:20,664 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:20,664 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,665 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,665 INFO  L85        PathProgramCache]: Analyzing trace with hash -345933610, now seen corresponding path program 1 times
[2025-04-28 21:21:20,665 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,665 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2029471480]
[2025-04-28 21:21:20,665 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,665 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,677 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:20,699 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:20,699 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,699 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,855 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:20,855 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,855 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2029471480]
[2025-04-28 21:21:20,855 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2029471480] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,855 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,855 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:20,856 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2017169422]
[2025-04-28 21:21:20,856 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,856 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:20,856 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,857 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:20,857 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:20,857 INFO  L87              Difference]: Start difference. First operand 32 states and 61 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:21,168 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,169 INFO  L93              Difference]: Finished difference Result 54 states and 113 transitions.
[2025-04-28 21:21:21,170 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:21,170 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:21:21,170 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,172 INFO  L225             Difference]: With dead ends: 54
[2025-04-28 21:21:21,172 INFO  L226             Difference]: Without dead ends: 54
[2025-04-28 21:21:21,172 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:21,177 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 6 mSDsluCounter, 75 mSDsCounter, 0 mSdLazyCounter, 140 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 106 SdHoareTripleChecker+Invalid, 145 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 140 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,177 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 106 Invalid, 145 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 140 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:21,178 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-04-28 21:21:21,200 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 44.
[2025-04-28 21:21:21,204 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 44 states, 17 states have (on average 1.7058823529411764) internal successors, (29), 27 states have internal predecessors, (29), 15 states have call successors, (15), 5 states have call predecessors, (15), 11 states have return successors, (47), 11 states have call predecessors, (47), 15 states have call successors, (47)
[2025-04-28 21:21:21,205 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 44 states to 44 states and 91 transitions.
[2025-04-28 21:21:21,205 INFO  L79                 Accepts]: Start accepts. Automaton has 44 states and 91 transitions. Word has length 17
[2025-04-28 21:21:21,206 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,206 INFO  L485      AbstractCegarLoop]: Abstraction has 44 states and 91 transitions.
[2025-04-28 21:21:21,206 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:21,206 INFO  L278                IsEmpty]: Start isEmpty. Operand 44 states and 91 transitions.
[2025-04-28 21:21:21,210 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:21,210 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,211 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,211 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:21,211 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,211 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,212 INFO  L85        PathProgramCache]: Analyzing trace with hash 1902810099, now seen corresponding path program 1 times
[2025-04-28 21:21:21,212 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,212 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1050549935]
[2025-04-28 21:21:21,212 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,212 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,220 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:21,234 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:21,234 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,234 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,343 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:21,343 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,343 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1050549935]
[2025-04-28 21:21:21,344 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1050549935] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,344 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,344 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:21,344 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1006826386]
[2025-04-28 21:21:21,344 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,344 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:21,344 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,345 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:21,345 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:21,345 INFO  L87              Difference]: Start difference. First operand 44 states and 91 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:21,558 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,558 INFO  L93              Difference]: Finished difference Result 54 states and 104 transitions.
[2025-04-28 21:21:21,560 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:21,560 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:21:21,560 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,561 INFO  L225             Difference]: With dead ends: 54
[2025-04-28 21:21:21,561 INFO  L226             Difference]: Without dead ends: 54
[2025-04-28 21:21:21,562 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:21,562 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 6 mSDsluCounter, 67 mSDsCounter, 0 mSdLazyCounter, 115 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 95 SdHoareTripleChecker+Invalid, 123 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 115 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,567 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 95 Invalid, 123 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 115 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:21,567 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-04-28 21:21:21,587 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 42.
[2025-04-28 21:21:21,587 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 42 states, 16 states have (on average 1.75) internal successors, (28), 26 states have internal predecessors, (28), 15 states have call successors, (15), 5 states have call predecessors, (15), 10 states have return successors, (35), 10 states have call predecessors, (35), 15 states have call successors, (35)
[2025-04-28 21:21:21,589 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 42 states to 42 states and 78 transitions.
[2025-04-28 21:21:21,589 INFO  L79                 Accepts]: Start accepts. Automaton has 42 states and 78 transitions. Word has length 17
[2025-04-28 21:21:21,589 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,589 INFO  L485      AbstractCegarLoop]: Abstraction has 42 states and 78 transitions.
[2025-04-28 21:21:21,589 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:21,589 INFO  L278                IsEmpty]: Start isEmpty. Operand 42 states and 78 transitions.
[2025-04-28 21:21:21,593 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:21,593 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,593 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,593 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:21,593 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,594 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,594 INFO  L85        PathProgramCache]: Analyzing trace with hash -1306051073, now seen corresponding path program 1 times
[2025-04-28 21:21:21,594 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,594 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [450703264]
[2025-04-28 21:21:21,594 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,594 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,601 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:21,609 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:21,609 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,610 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,720 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:21,720 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,720 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [450703264]
[2025-04-28 21:21:21,721 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [450703264] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:21,721 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [3789723]
[2025-04-28 21:21:21,721 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,721 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:21,724 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:21,726 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:21,730 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:21,770 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:21,786 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:21,786 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,786 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,791 INFO  L256         TraceCheckSpWp]: Trace formula consists of 81 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:21,793 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:21,877 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:21,879 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:22,388 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:22,391 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [3789723] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:22,392 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:22,392 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:22,392 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [213758008]
[2025-04-28 21:21:22,392 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:22,392 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:22,392 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:22,393 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:22,393 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:22,394 INFO  L87              Difference]: Start difference. First operand 42 states and 78 transitions. Second operand  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:22,623 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:22,625 INFO  L93              Difference]: Finished difference Result 62 states and 123 transitions.
[2025-04-28 21:21:22,626 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:22,626 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9) Word has length 17
[2025-04-28 21:21:22,626 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:22,627 INFO  L225             Difference]: With dead ends: 62
[2025-04-28 21:21:22,629 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:22,630 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 42 GetRequests, 28 SyntacticMatches, 3 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 15 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:22,630 INFO  L437           NwaCegarLoop]: 25 mSDtfsCounter, 6 mSDsluCounter, 118 mSDsCounter, 0 mSdLazyCounter, 143 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 143 SdHoareTripleChecker+Invalid, 161 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 143 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:22,631 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 143 Invalid, 161 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 143 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:22,631 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:22,648 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 46.
[2025-04-28 21:21:22,649 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 18 states have (on average 1.6666666666666667) internal successors, (30), 28 states have internal predecessors, (30), 15 states have call successors, (15), 5 states have call predecessors, (15), 12 states have return successors, (45), 12 states have call predecessors, (45), 15 states have call successors, (45)
[2025-04-28 21:21:22,650 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 90 transitions.
[2025-04-28 21:21:22,651 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 90 transitions. Word has length 17
[2025-04-28 21:21:22,652 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:22,652 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 90 transitions.
[2025-04-28 21:21:22,652 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:22,652 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 90 transitions.
[2025-04-28 21:21:22,654 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:22,656 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,656 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:22,662 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:22,857 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:22,857 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,857 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,857 INFO  L85        PathProgramCache]: Analyzing trace with hash -768919526, now seen corresponding path program 1 times
[2025-04-28 21:21:22,857 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,858 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1477991897]
[2025-04-28 21:21:22,858 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,858 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,862 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:22,868 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:22,868 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,868 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,990 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:22,990 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,990 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1477991897]
[2025-04-28 21:21:22,990 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1477991897] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:22,990 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [60486388]
[2025-04-28 21:21:22,990 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,990 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,993 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,995 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:22,997 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:23,027 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:23,044 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:23,044 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,044 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,046 INFO  L256         TraceCheckSpWp]: Trace formula consists of 85 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:23,047 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:23,189 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:23,190 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:23,653 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:23,653 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [60486388] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:23,653 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:23,654 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 17
[2025-04-28 21:21:23,654 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1406673600]
[2025-04-28 21:21:23,654 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:23,654 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:23,654 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:23,655 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:23,655 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=235, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:23,655 INFO  L87              Difference]: Start difference. First operand 46 states and 90 transitions. Second operand  has 17 states, 8 states have (on average 2.375) internal successors, (19), 16 states have internal predecessors, (19), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 5 states have call predecessors, (10), 10 states have call successors, (10)
[2025-04-28 21:21:24,324 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:24,324 INFO  L93              Difference]: Finished difference Result 84 states and 177 transitions.
[2025-04-28 21:21:24,325 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-04-28 21:21:24,325 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.375) internal successors, (19), 16 states have internal predecessors, (19), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 5 states have call predecessors, (10), 10 states have call successors, (10) Word has length 17
[2025-04-28 21:21:24,326 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:24,327 INFO  L225             Difference]: With dead ends: 84
[2025-04-28 21:21:24,327 INFO  L226             Difference]: Without dead ends: 76
[2025-04-28 21:21:24,328 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 53 GetRequests, 24 SyntacticMatches, 2 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 82 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=116, Invalid=696, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:21:24,329 INFO  L437           NwaCegarLoop]: 25 mSDtfsCounter, 15 mSDsluCounter, 246 mSDsCounter, 0 mSdLazyCounter, 302 mSolverCounterSat, 69 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 271 SdHoareTripleChecker+Invalid, 371 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 69 IncrementalHoareTripleChecker+Valid, 302 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:24,329 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 271 Invalid, 371 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [69 Valid, 302 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:24,330 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 76 states.
[2025-04-28 21:21:24,342 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 76 to 50.
[2025-04-28 21:21:24,342 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 20 states have (on average 1.6) internal successors, (32), 30 states have internal predecessors, (32), 15 states have call successors, (15), 5 states have call predecessors, (15), 14 states have return successors, (53), 14 states have call predecessors, (53), 15 states have call successors, (53)
[2025-04-28 21:21:24,343 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 100 transitions.
[2025-04-28 21:21:24,343 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 100 transitions. Word has length 17
[2025-04-28 21:21:24,344 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:24,344 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 100 transitions.
[2025-04-28 21:21:24,344 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.375) internal successors, (19), 16 states have internal predecessors, (19), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 5 states have call predecessors, (10), 10 states have call successors, (10)
[2025-04-28 21:21:24,344 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 100 transitions.
[2025-04-28 21:21:24,345 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:24,346 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,346 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:24,352 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:24,546 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:21:24,547 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,547 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,548 INFO  L85        PathProgramCache]: Analyzing trace with hash -231787979, now seen corresponding path program 1 times
[2025-04-28 21:21:24,548 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,548 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [815707426]
[2025-04-28 21:21:24,548 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,548 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,552 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:24,556 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:24,557 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,557 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,633 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:24,634 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,634 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [815707426]
[2025-04-28 21:21:24,634 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [815707426] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:24,634 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1117888464]
[2025-04-28 21:21:24,634 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,634 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:24,637 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:24,639 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:21:24,643 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:24,688 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:24,704 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:24,704 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,704 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,705 INFO  L256         TraceCheckSpWp]: Trace formula consists of 81 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:24,706 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:24,766 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:24,767 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:25,152 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:25,152 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1117888464] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:25,152 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:25,152 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:25,153 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1774504396]
[2025-04-28 21:21:25,153 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,153 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:25,153 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,154 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:25,154 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:25,154 INFO  L87              Difference]: Start difference. First operand 50 states and 100 transitions. Second operand  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:25,351 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,352 INFO  L93              Difference]: Finished difference Result 62 states and 129 transitions.
[2025-04-28 21:21:25,352 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:25,352 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9) Word has length 17
[2025-04-28 21:21:25,352 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,353 INFO  L225             Difference]: With dead ends: 62
[2025-04-28 21:21:25,353 INFO  L226             Difference]: Without dead ends: 62
[2025-04-28 21:21:25,354 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 42 GetRequests, 28 SyntacticMatches, 3 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 15 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:25,354 INFO  L437           NwaCegarLoop]: 26 mSDtfsCounter, 5 mSDsluCounter, 132 mSDsCounter, 0 mSdLazyCounter, 152 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 158 SdHoareTripleChecker+Invalid, 167 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 152 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:25,355 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 158 Invalid, 167 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 152 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:25,355 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-04-28 21:21:25,363 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 46.
[2025-04-28 21:21:25,364 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 18 states have (on average 1.6666666666666667) internal successors, (30), 28 states have internal predecessors, (30), 15 states have call successors, (15), 5 states have call predecessors, (15), 12 states have return successors, (45), 12 states have call predecessors, (45), 15 states have call successors, (45)
[2025-04-28 21:21:25,364 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 90 transitions.
[2025-04-28 21:21:25,365 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 90 transitions. Word has length 17
[2025-04-28 21:21:25,365 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,365 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 90 transitions.
[2025-04-28 21:21:25,365 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:25,365 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 90 transitions.
[2025-04-28 21:21:25,366 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:25,366 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,366 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:25,371 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:25,566 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:21:25,567 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,567 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,567 INFO  L85        PathProgramCache]: Analyzing trace with hash -695661873, now seen corresponding path program 2 times
[2025-04-28 21:21:25,567 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,567 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [7289075]
[2025-04-28 21:21:25,567 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:25,568 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,572 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:21:25,577 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:25,577 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:25,578 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,663 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:25,663 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,663 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [7289075]
[2025-04-28 21:21:25,663 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [7289075] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:25,663 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [54602612]
[2025-04-28 21:21:25,664 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:25,664 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,666 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:25,668 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:21:25,671 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:25,712 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:21:25,730 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:25,730 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:25,730 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,732 INFO  L256         TraceCheckSpWp]: Trace formula consists of 103 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:25,733 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:25,825 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:25,825 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:26,533 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:26,534 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [54602612] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:26,534 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:26,534 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 14
[2025-04-28 21:21:26,534 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1445593528]
[2025-04-28 21:21:26,534 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,534 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:26,535 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,535 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:26,535 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=145, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:26,535 INFO  L87              Difference]: Start difference. First operand 46 states and 90 transitions. Second operand  has 14 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:26,907 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,908 INFO  L93              Difference]: Finished difference Result 74 states and 135 transitions.
[2025-04-28 21:21:26,908 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:26,908 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11) Word has length 21
[2025-04-28 21:21:26,909 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,909 INFO  L225             Difference]: With dead ends: 74
[2025-04-28 21:21:26,909 INFO  L226             Difference]: Without dead ends: 62
[2025-04-28 21:21:26,910 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 55 GetRequests, 36 SyntacticMatches, 1 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 44 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=90, Invalid=290, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:26,911 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 16 mSDsluCounter, 135 mSDsCounter, 0 mSdLazyCounter, 238 mSolverCounterSat, 44 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 164 SdHoareTripleChecker+Invalid, 282 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 44 IncrementalHoareTripleChecker+Valid, 238 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,911 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 164 Invalid, 282 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [44 Valid, 238 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:26,912 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-04-28 21:21:26,919 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 50.
[2025-04-28 21:21:26,920 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 20 states have (on average 1.65) internal successors, (33), 30 states have internal predecessors, (33), 16 states have call successors, (16), 6 states have call predecessors, (16), 13 states have return successors, (46), 13 states have call predecessors, (46), 16 states have call successors, (46)
[2025-04-28 21:21:26,920 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 95 transitions.
[2025-04-28 21:21:26,921 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 95 transitions. Word has length 21
[2025-04-28 21:21:26,921 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,921 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 95 transitions.
[2025-04-28 21:21:26,921 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:26,921 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 95 transitions.
[2025-04-28 21:21:26,922 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:26,922 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,922 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,930 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:27,126 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:21:27,126 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,127 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,127 INFO  L85        PathProgramCache]: Analyzing trace with hash -792403804, now seen corresponding path program 1 times
[2025-04-28 21:21:27,127 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,127 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2087418829]
[2025-04-28 21:21:27,127 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,127 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,131 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:27,138 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:27,138 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,138 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,248 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:27,248 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,248 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2087418829]
[2025-04-28 21:21:27,248 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2087418829] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,248 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1423039692]
[2025-04-28 21:21:27,248 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,248 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,251 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,253 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:21:27,257 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:27,305 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:27,321 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:27,321 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,321 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,323 INFO  L256         TraceCheckSpWp]: Trace formula consists of 103 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:27,324 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,436 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:27,437 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:28,603 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:28,603 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1423039692] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,603 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:28,603 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [8, 8] total 15
[2025-04-28 21:21:28,603 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1434455762]
[2025-04-28 21:21:28,603 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,604 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:28,604 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,605 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:28,605 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=41, Invalid=169, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:28,605 INFO  L87              Difference]: Start difference. First operand 50 states and 95 transitions. Second operand  has 8 states, 5 states have (on average 2.0) internal successors, (10), 8 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:28,731 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,731 INFO  L93              Difference]: Finished difference Result 62 states and 115 transitions.
[2025-04-28 21:21:28,732 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:28,732 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.0) internal successors, (10), 8 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5) Word has length 21
[2025-04-28 21:21:28,732 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,733 INFO  L225             Difference]: With dead ends: 62
[2025-04-28 21:21:28,733 INFO  L226             Difference]: Without dead ends: 62
[2025-04-28 21:21:28,733 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 50 GetRequests, 34 SyntacticMatches, 3 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 28 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=41, Invalid=169, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:28,734 INFO  L437           NwaCegarLoop]: 25 mSDtfsCounter, 2 mSDsluCounter, 86 mSDsCounter, 0 mSdLazyCounter, 89 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 111 SdHoareTripleChecker+Invalid, 92 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 89 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,734 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 111 Invalid, 92 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 89 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:28,734 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-04-28 21:21:28,746 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 46.
[2025-04-28 21:21:28,746 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 18 states have (on average 1.7222222222222223) internal successors, (31), 28 states have internal predecessors, (31), 16 states have call successors, (16), 6 states have call predecessors, (16), 11 states have return successors, (34), 11 states have call predecessors, (34), 16 states have call successors, (34)
[2025-04-28 21:21:28,747 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 81 transitions.
[2025-04-28 21:21:28,748 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 81 transitions. Word has length 21
[2025-04-28 21:21:28,749 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,749 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 81 transitions.
[2025-04-28 21:21:28,749 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.0) internal successors, (10), 8 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:28,749 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 81 transitions.
[2025-04-28 21:21:28,750 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:28,752 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,752 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,758 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:28,953 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:21:28,953 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,953 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,953 INFO  L85        PathProgramCache]: Analyzing trace with hash -1019743167, now seen corresponding path program 1 times
[2025-04-28 21:21:28,953 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,953 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1461731873]
[2025-04-28 21:21:28,953 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,953 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,957 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:28,963 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:28,963 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,963 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,111 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:29,111 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,111 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1461731873]
[2025-04-28 21:21:29,111 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1461731873] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,111 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1281890302]
[2025-04-28 21:21:29,111 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,111 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,114 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,116 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:29,119 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,170 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:29,186 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:29,186 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,186 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,187 INFO  L256         TraceCheckSpWp]: Trace formula consists of 107 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,189 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,303 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:29,303 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:30,364 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:30,365 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1281890302] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:30,365 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:30,365 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 15
[2025-04-28 21:21:30,365 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1857655396]
[2025-04-28 21:21:30,365 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,365 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:30,365 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,366 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:30,368 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=172, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:30,369 INFO  L87              Difference]: Start difference. First operand 46 states and 81 transitions. Second operand  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 15 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (11), 6 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:30,589 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,590 INFO  L93              Difference]: Finished difference Result 72 states and 122 transitions.
[2025-04-28 21:21:30,590 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:30,590 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 15 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (11), 6 states have call predecessors, (11), 9 states have call successors, (11) Word has length 21
[2025-04-28 21:21:30,591 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,592 INFO  L225             Difference]: With dead ends: 72
[2025-04-28 21:21:30,592 INFO  L226             Difference]: Without dead ends: 68
[2025-04-28 21:21:30,593 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 51 GetRequests, 34 SyntacticMatches, 3 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 31 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=45, Invalid=195, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:30,594 INFO  L437           NwaCegarLoop]: 25 mSDtfsCounter, 6 mSDsluCounter, 173 mSDsCounter, 0 mSdLazyCounter, 189 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 198 SdHoareTripleChecker+Invalid, 199 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 189 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,595 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 198 Invalid, 199 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 189 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:30,596 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 68 states.
[2025-04-28 21:21:30,606 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 68 to 48.
[2025-04-28 21:21:30,610 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 19 states have (on average 1.6842105263157894) internal successors, (32), 29 states have internal predecessors, (32), 16 states have call successors, (16), 6 states have call predecessors, (16), 12 states have return successors, (37), 12 states have call predecessors, (37), 16 states have call successors, (37)
[2025-04-28 21:21:30,611 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 85 transitions.
[2025-04-28 21:21:30,611 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 85 transitions. Word has length 21
[2025-04-28 21:21:30,611 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,611 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 85 transitions.
[2025-04-28 21:21:30,611 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 15 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (11), 6 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:30,611 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 85 transitions.
[2025-04-28 21:21:30,612 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:30,612 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,612 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,619 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:30,812 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable10
[2025-04-28 21:21:30,813 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,813 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,813 INFO  L85        PathProgramCache]: Analyzing trace with hash 930279332, now seen corresponding path program 1 times
[2025-04-28 21:21:30,813 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,813 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1650493447]
[2025-04-28 21:21:30,813 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,814 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,817 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:30,821 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:30,822 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,822 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,939 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:30,939 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,939 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1650493447]
[2025-04-28 21:21:30,940 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1650493447] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,940 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1989497443]
[2025-04-28 21:21:30,940 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,940 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,942 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,944 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:30,949 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,007 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:31,021 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:31,021 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,021 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,022 INFO  L256         TraceCheckSpWp]: Trace formula consists of 103 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,023 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,093 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:31,093 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:31,671 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:31,671 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1989497443] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:31,671 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:31,671 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 16
[2025-04-28 21:21:31,671 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1256232946]
[2025-04-28 21:21:31,671 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,672 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:31,672 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,672 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:31,672 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=45, Invalid=195, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:31,672 INFO  L87              Difference]: Start difference. First operand 48 states and 85 transitions. Second operand  has 16 states, 8 states have (on average 2.125) internal successors, (17), 15 states have internal predecessors, (17), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:31,898 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,898 INFO  L93              Difference]: Finished difference Result 76 states and 141 transitions.
[2025-04-28 21:21:31,898 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:31,899 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.125) internal successors, (17), 15 states have internal predecessors, (17), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12) Word has length 21
[2025-04-28 21:21:31,899 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,899 INFO  L225             Difference]: With dead ends: 76
[2025-04-28 21:21:31,899 INFO  L226             Difference]: Without dead ends: 74
[2025-04-28 21:21:31,900 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 53 GetRequests, 34 SyntacticMatches, 3 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 41 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=56, Invalid=250, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:31,900 INFO  L437           NwaCegarLoop]: 25 mSDtfsCounter, 7 mSDsluCounter, 170 mSDsCounter, 0 mSdLazyCounter, 216 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 195 SdHoareTripleChecker+Invalid, 227 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 216 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,900 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 195 Invalid, 227 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 216 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:31,901 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 74 states.
[2025-04-28 21:21:31,908 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 74 to 50.
[2025-04-28 21:21:31,908 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 20 states have (on average 1.65) internal successors, (33), 30 states have internal predecessors, (33), 16 states have call successors, (16), 6 states have call predecessors, (16), 13 states have return successors, (38), 13 states have call predecessors, (38), 16 states have call successors, (38)
[2025-04-28 21:21:31,909 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 87 transitions.
[2025-04-28 21:21:31,909 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 87 transitions. Word has length 21
[2025-04-28 21:21:31,909 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,909 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 87 transitions.
[2025-04-28 21:21:31,909 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.125) internal successors, (17), 15 states have internal predecessors, (17), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:31,909 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 87 transitions.
[2025-04-28 21:21:31,910 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:31,910 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,910 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,918 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:32,114 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-04-28 21:21:32,114 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,115 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,115 INFO  L85        PathProgramCache]: Analyzing trace with hash -2072385405, now seen corresponding path program 2 times
[2025-04-28 21:21:32,115 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,115 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [486513734]
[2025-04-28 21:21:32,115 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:32,115 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,119 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:32,125 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:32,125 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:32,125 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,240 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:32,240 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,240 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [486513734]
[2025-04-28 21:21:32,240 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [486513734] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:32,240 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2044217095]
[2025-04-28 21:21:32,240 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:32,240 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,243 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:32,245 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:32,249 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:32,308 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:32,327 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:32,327 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:32,327 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,328 INFO  L256         TraceCheckSpWp]: Trace formula consists of 133 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:32,329 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,466 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:32,466 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,358 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:33,358 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2044217095] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,358 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,358 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 10, 10] total 20
[2025-04-28 21:21:33,358 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1427904773]
[2025-04-28 21:21:33,358 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,359 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:33,359 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,359 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:33,360 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=49, Invalid=331, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:33,360 INFO  L87              Difference]: Start difference. First operand 50 states and 87 transitions. Second operand  has 20 states, 9 states have (on average 2.7777777777777777) internal successors, (25), 20 states have internal predecessors, (25), 12 states have call successors, (14), 1 states have call predecessors, (14), 8 states have return successors, (14), 7 states have call predecessors, (14), 12 states have call successors, (14)
[2025-04-28 21:21:34,090 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,090 INFO  L93              Difference]: Finished difference Result 100 states and 158 transitions.
[2025-04-28 21:21:34,091 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 24 states. 
[2025-04-28 21:21:34,091 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 9 states have (on average 2.7777777777777777) internal successors, (25), 20 states have internal predecessors, (25), 12 states have call successors, (14), 1 states have call predecessors, (14), 8 states have return successors, (14), 7 states have call predecessors, (14), 12 states have call successors, (14) Word has length 25
[2025-04-28 21:21:34,091 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,092 INFO  L225             Difference]: With dead ends: 100
[2025-04-28 21:21:34,092 INFO  L226             Difference]: Without dead ends: 81
[2025-04-28 21:21:34,092 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 74 GetRequests, 38 SyntacticMatches, 2 SemanticMatches, 34 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 169 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=187, Invalid=1073, Unknown=0, NotChecked=0, Total=1260
[2025-04-28 21:21:34,093 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 16 mSDsluCounter, 288 mSDsCounter, 0 mSdLazyCounter, 472 mSolverCounterSat, 43 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 324 SdHoareTripleChecker+Invalid, 515 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 43 IncrementalHoareTripleChecker+Valid, 472 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,093 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 324 Invalid, 515 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [43 Valid, 472 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:34,094 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 81 states.
[2025-04-28 21:21:34,101 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 81 to 51.
[2025-04-28 21:21:34,101 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 51 states, 21 states have (on average 1.5714285714285714) internal successors, (33), 30 states have internal predecessors, (33), 15 states have call successors, (15), 6 states have call predecessors, (15), 14 states have return successors, (37), 14 states have call predecessors, (37), 15 states have call successors, (37)
[2025-04-28 21:21:34,103 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 51 states to 51 states and 85 transitions.
[2025-04-28 21:21:34,103 INFO  L79                 Accepts]: Start accepts. Automaton has 51 states and 85 transitions. Word has length 25
[2025-04-28 21:21:34,103 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,103 INFO  L485      AbstractCegarLoop]: Abstraction has 51 states and 85 transitions.
[2025-04-28 21:21:34,104 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 9 states have (on average 2.7777777777777777) internal successors, (25), 20 states have internal predecessors, (25), 12 states have call successors, (14), 1 states have call predecessors, (14), 8 states have return successors, (14), 7 states have call predecessors, (14), 12 states have call successors, (14)
[2025-04-28 21:21:34,104 INFO  L278                IsEmpty]: Start isEmpty. Operand 51 states and 85 transitions.
[2025-04-28 21:21:34,105 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:34,105 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,105 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 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:34,112 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:34,305 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:34,305 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,306 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,306 INFO  L85        PathProgramCache]: Analyzing trace with hash 1507629488, now seen corresponding path program 1 times
[2025-04-28 21:21:34,306 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,306 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [74532489]
[2025-04-28 21:21:34,306 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,306 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,316 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:34,322 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:34,322 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,322 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,424 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:34,424 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,424 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [74532489]
[2025-04-28 21:21:34,424 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [74532489] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:34,424 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:34,424 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:34,425 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [753762547]
[2025-04-28 21:21:34,425 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,425 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:34,426 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,426 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:34,426 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:34,427 INFO  L87              Difference]: Start difference. First operand 51 states and 85 transitions. Second operand  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:34,587 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,587 INFO  L93              Difference]: Finished difference Result 63 states and 98 transitions.
[2025-04-28 21:21:34,588 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:34,588 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6) Word has length 25
[2025-04-28 21:21:34,588 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,589 INFO  L225             Difference]: With dead ends: 63
[2025-04-28 21:21:34,589 INFO  L226             Difference]: Without dead ends: 59
[2025-04-28 21:21:34,589 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:34,590 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 5 mSDsluCounter, 103 mSDsCounter, 0 mSdLazyCounter, 147 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 131 SdHoareTripleChecker+Invalid, 150 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 147 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,590 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 131 Invalid, 150 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 147 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:34,590 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 59 states.
[2025-04-28 21:21:34,601 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 59 to 51.
[2025-04-28 21:21:34,601 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 51 states, 21 states have (on average 1.5714285714285714) internal successors, (33), 30 states have internal predecessors, (33), 15 states have call successors, (15), 6 states have call predecessors, (15), 14 states have return successors, (35), 14 states have call predecessors, (35), 15 states have call successors, (35)
[2025-04-28 21:21:34,602 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 51 states to 51 states and 83 transitions.
[2025-04-28 21:21:34,602 INFO  L79                 Accepts]: Start accepts. Automaton has 51 states and 83 transitions. Word has length 25
[2025-04-28 21:21:34,602 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,602 INFO  L485      AbstractCegarLoop]: Abstraction has 51 states and 83 transitions.
[2025-04-28 21:21:34,602 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:34,602 INFO  L278                IsEmpty]: Start isEmpty. Operand 51 states and 83 transitions.
[2025-04-28 21:21:34,603 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:34,603 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,603 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,603 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:34,604 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,607 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,607 INFO  L85        PathProgramCache]: Analyzing trace with hash -1351787234, now seen corresponding path program 1 times
[2025-04-28 21:21:34,607 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,607 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [703801162]
[2025-04-28 21:21:34,608 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,608 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,617 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:34,627 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:34,627 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,627 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,755 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:34,755 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,755 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [703801162]
[2025-04-28 21:21:34,755 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [703801162] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,755 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [138550857]
[2025-04-28 21:21:34,755 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,755 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,757 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,760 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:34,764 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,833 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:34,854 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:34,854 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,854 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,855 INFO  L256         TraceCheckSpWp]: Trace formula consists of 137 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,856 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,936 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:34,937 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:35,781 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 3 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:35,781 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [138550857] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:35,781 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:35,781 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 17
[2025-04-28 21:21:35,781 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2116336927]
[2025-04-28 21:21:35,782 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,782 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:35,782 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,782 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:35,782 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=47, Invalid=225, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:35,783 INFO  L87              Difference]: Start difference. First operand 51 states and 83 transitions. Second operand  has 17 states, 8 states have (on average 2.5) internal successors, (20), 17 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (13), 6 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:36,238 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,238 INFO  L93              Difference]: Finished difference Result 85 states and 133 transitions.
[2025-04-28 21:21:36,238 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:21:36,239 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 17 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (13), 6 states have call predecessors, (13), 10 states have call successors, (13) Word has length 25
[2025-04-28 21:21:36,239 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,240 INFO  L225             Difference]: With dead ends: 85
[2025-04-28 21:21:36,240 INFO  L226             Difference]: Without dead ends: 83
[2025-04-28 21:21:36,240 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 69 GetRequests, 42 SyntacticMatches, 2 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 100 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=139, Invalid=563, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:36,241 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 24 mSDsluCounter, 186 mSDsCounter, 0 mSdLazyCounter, 322 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 33 SdHoareTripleChecker+Valid, 213 SdHoareTripleChecker+Invalid, 363 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 322 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,241 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [33 Valid, 213 Invalid, 363 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 322 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:36,242 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 83 states.
[2025-04-28 21:21:36,248 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 83 to 51.
[2025-04-28 21:21:36,249 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 51 states, 21 states have (on average 1.5714285714285714) internal successors, (33), 30 states have internal predecessors, (33), 15 states have call successors, (15), 6 states have call predecessors, (15), 14 states have return successors, (35), 14 states have call predecessors, (35), 15 states have call successors, (35)
[2025-04-28 21:21:36,249 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 51 states to 51 states and 83 transitions.
[2025-04-28 21:21:36,249 INFO  L79                 Accepts]: Start accepts. Automaton has 51 states and 83 transitions. Word has length 25
[2025-04-28 21:21:36,249 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,249 INFO  L485      AbstractCegarLoop]: Abstraction has 51 states and 83 transitions.
[2025-04-28 21:21:36,250 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 17 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (13), 6 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:36,252 INFO  L278                IsEmpty]: Start isEmpty. Operand 51 states and 83 transitions.
[2025-04-28 21:21:36,254 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:36,255 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,255 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 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:36,261 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-04-28 21:21:36,455 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,456 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,456 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,456 INFO  L85        PathProgramCache]: Analyzing trace with hash -2066739637, now seen corresponding path program 1 times
[2025-04-28 21:21:36,456 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,456 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1354131651]
[2025-04-28 21:21:36,456 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,456 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,461 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:36,467 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:36,467 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,467 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,783 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:36,783 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,783 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1354131651]
[2025-04-28 21:21:36,783 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1354131651] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,783 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2053584717]
[2025-04-28 21:21:36,783 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,783 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,786 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,788 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:36,791 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,877 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:36,902 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:36,902 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,902 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,904 INFO  L256         TraceCheckSpWp]: Trace formula consists of 133 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,907 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,197 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:37,198 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,273 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:38,273 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2053584717] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,273 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,273 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 12, 12] total 24
[2025-04-28 21:21:38,274 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [174680028]
[2025-04-28 21:21:38,274 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,274 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:38,274 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,275 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:38,275 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=70, Invalid=482, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:38,275 INFO  L87              Difference]: Start difference. First operand 51 states and 83 transitions. Second operand  has 24 states, 11 states have (on average 2.3636363636363638) internal successors, (26), 23 states have internal predecessors, (26), 14 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (16), 9 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:21:39,199 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,199 INFO  L93              Difference]: Finished difference Result 95 states and 150 transitions.
[2025-04-28 21:21:39,200 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 23 states. 
[2025-04-28 21:21:39,200 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 11 states have (on average 2.3636363636363638) internal successors, (26), 23 states have internal predecessors, (26), 14 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (16), 9 states have call predecessors, (16), 14 states have call successors, (16) Word has length 25
[2025-04-28 21:21:39,200 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,201 INFO  L225             Difference]: With dead ends: 95
[2025-04-28 21:21:39,202 INFO  L226             Difference]: Without dead ends: 91
[2025-04-28 21:21:39,202 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 74 GetRequests, 39 SyntacticMatches, 0 SemanticMatches, 35 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 235 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=167, Invalid=1165, Unknown=0, NotChecked=0, Total=1332
[2025-04-28 21:21:39,203 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 23 mSDsluCounter, 331 mSDsCounter, 0 mSdLazyCounter, 638 mSolverCounterSat, 17 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 44 SdHoareTripleChecker+Valid, 355 SdHoareTripleChecker+Invalid, 655 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 17 IncrementalHoareTripleChecker+Valid, 638 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,203 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [44 Valid, 355 Invalid, 655 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [17 Valid, 638 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:39,204 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-04-28 21:21:39,211 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 59.
[2025-04-28 21:21:39,211 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 59 states, 25 states have (on average 1.48) internal successors, (37), 34 states have internal predecessors, (37), 15 states have call successors, (15), 6 states have call predecessors, (15), 18 states have return successors, (46), 18 states have call predecessors, (46), 15 states have call successors, (46)
[2025-04-28 21:21:39,212 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 59 states to 59 states and 98 transitions.
[2025-04-28 21:21:39,212 INFO  L79                 Accepts]: Start accepts. Automaton has 59 states and 98 transitions. Word has length 25
[2025-04-28 21:21:39,212 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,212 INFO  L485      AbstractCegarLoop]: Abstraction has 59 states and 98 transitions.
[2025-04-28 21:21:39,213 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 11 states have (on average 2.3636363636363638) internal successors, (26), 23 states have internal predecessors, (26), 14 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (16), 9 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:21:39,213 INFO  L278                IsEmpty]: Start isEmpty. Operand 59 states and 98 transitions.
[2025-04-28 21:21:39,214 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:39,214 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,214 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,223 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:39,414 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-04-28 21:21:39,415 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,415 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,415 INFO  L85        PathProgramCache]: Analyzing trace with hash -1421457325, now seen corresponding path program 2 times
[2025-04-28 21:21:39,415 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,415 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [90843000]
[2025-04-28 21:21:39,415 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:39,415 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,420 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:39,425 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:39,426 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:39,426 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,596 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:39,596 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,596 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [90843000]
[2025-04-28 21:21:39,596 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [90843000] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,596 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [234906429]
[2025-04-28 21:21:39,596 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:39,596 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,598 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,599 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:39,601 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,680 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:39,698 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:39,698 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:39,698 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,699 INFO  L256         TraceCheckSpWp]: Trace formula consists of 125 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,700 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,835 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:39,835 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:41,841 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:41,841 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [234906429] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:41,841 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:41,841 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 21
[2025-04-28 21:21:41,842 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1768481200]
[2025-04-28 21:21:41,842 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,842 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:41,842 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,843 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:41,843 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=70, Invalid=350, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:41,843 INFO  L87              Difference]: Start difference. First operand 59 states and 98 transitions. Second operand  has 21 states, 12 states have (on average 2.0) internal successors, (24), 21 states have internal predecessors, (24), 10 states have call successors, (11), 1 states have call predecessors, (11), 11 states have return successors, (15), 11 states have call predecessors, (15), 10 states have call successors, (15)
[2025-04-28 21:21:42,110 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,110 INFO  L93              Difference]: Finished difference Result 75 states and 117 transitions.
[2025-04-28 21:21:42,111 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:42,111 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 12 states have (on average 2.0) internal successors, (24), 21 states have internal predecessors, (24), 10 states have call successors, (11), 1 states have call predecessors, (11), 11 states have return successors, (15), 11 states have call predecessors, (15), 10 states have call successors, (15) Word has length 25
[2025-04-28 21:21:42,111 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,112 INFO  L225             Difference]: With dead ends: 75
[2025-04-28 21:21:42,113 INFO  L226             Difference]: Without dead ends: 66
[2025-04-28 21:21:42,113 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 64 GetRequests, 39 SyntacticMatches, 3 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 85 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=111, Invalid=441, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:42,114 INFO  L437           NwaCegarLoop]: 26 mSDtfsCounter, 6 mSDsluCounter, 210 mSDsCounter, 0 mSdLazyCounter, 226 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 236 SdHoareTripleChecker+Invalid, 239 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 226 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,114 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 236 Invalid, 239 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 226 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:42,114 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 66 states.
[2025-04-28 21:21:42,119 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 66 to 58.
[2025-04-28 21:21:42,120 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 58 states, 25 states have (on average 1.44) internal successors, (36), 33 states have internal predecessors, (36), 14 states have call successors, (14), 6 states have call predecessors, (14), 18 states have return successors, (45), 18 states have call predecessors, (45), 14 states have call successors, (45)
[2025-04-28 21:21:42,121 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 95 transitions.
[2025-04-28 21:21:42,121 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 95 transitions. Word has length 25
[2025-04-28 21:21:42,121 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,122 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 95 transitions.
[2025-04-28 21:21:42,122 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 12 states have (on average 2.0) internal successors, (24), 21 states have internal predecessors, (24), 10 states have call successors, (11), 1 states have call predecessors, (11), 11 states have return successors, (15), 11 states have call predecessors, (15), 10 states have call successors, (15)
[2025-04-28 21:21:42,122 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 95 transitions.
[2025-04-28 21:21:42,124 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:42,124 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,125 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 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:42,131 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Ended with exit code 0
[2025-04-28 21:21:42,325 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 13 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable16
[2025-04-28 21:21:42,325 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,326 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,326 INFO  L85        PathProgramCache]: Analyzing trace with hash 1661452980, now seen corresponding path program 1 times
[2025-04-28 21:21:42,326 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,326 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2091507368]
[2025-04-28 21:21:42,326 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,326 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,331 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:42,338 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:42,338 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,338 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,373 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:42,373 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,373 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2091507368]
[2025-04-28 21:21:42,373 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2091507368] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,373 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,373 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:42,374 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [341429175]
[2025-04-28 21:21:42,374 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,374 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:42,374 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,374 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:42,375 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:42,375 INFO  L87              Difference]: Start difference. First operand 58 states and 95 transitions. Second operand  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:42,459 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,460 INFO  L93              Difference]: Finished difference Result 81 states and 141 transitions.
[2025-04-28 21:21:42,460 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:42,460 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7) Word has length 29
[2025-04-28 21:21:42,461 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,462 INFO  L225             Difference]: With dead ends: 81
[2025-04-28 21:21:42,462 INFO  L226             Difference]: Without dead ends: 81
[2025-04-28 21:21:42,462 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:42,463 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 5 mSDsluCounter, 44 mSDsCounter, 0 mSdLazyCounter, 48 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 79 SdHoareTripleChecker+Invalid, 51 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 48 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,463 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 79 Invalid, 51 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 48 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:42,464 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 81 states.
[2025-04-28 21:21:42,469 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 81 to 69.
[2025-04-28 21:21:42,470 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 69 states, 30 states have (on average 1.4666666666666666) internal successors, (44), 40 states have internal predecessors, (44), 16 states have call successors, (16), 7 states have call predecessors, (16), 22 states have return successors, (59), 21 states have call predecessors, (59), 16 states have call successors, (59)
[2025-04-28 21:21:42,470 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 69 states to 69 states and 119 transitions.
[2025-04-28 21:21:42,470 INFO  L79                 Accepts]: Start accepts. Automaton has 69 states and 119 transitions. Word has length 29
[2025-04-28 21:21:42,471 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,471 INFO  L485      AbstractCegarLoop]: Abstraction has 69 states and 119 transitions.
[2025-04-28 21:21:42,471 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:42,471 INFO  L278                IsEmpty]: Start isEmpty. Operand 69 states and 119 transitions.
[2025-04-28 21:21:42,472 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:42,472 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,472 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 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:42,472 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:21:42,472 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,473 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,473 INFO  L85        PathProgramCache]: Analyzing trace with hash 841385113, now seen corresponding path program 1 times
[2025-04-28 21:21:42,473 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,473 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1369526713]
[2025-04-28 21:21:42,473 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,473 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,478 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:42,484 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:42,484 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,485 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,519 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:42,520 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,520 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1369526713]
[2025-04-28 21:21:42,520 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1369526713] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,520 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,520 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:42,520 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2041021118]
[2025-04-28 21:21:42,520 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,520 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:42,521 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,521 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:42,521 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:42,521 INFO  L87              Difference]: Start difference. First operand 69 states and 119 transitions. Second operand  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:42,598 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,598 INFO  L93              Difference]: Finished difference Result 79 states and 131 transitions.
[2025-04-28 21:21:42,599 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:42,599 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7) Word has length 29
[2025-04-28 21:21:42,599 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,600 INFO  L225             Difference]: With dead ends: 79
[2025-04-28 21:21:42,600 INFO  L226             Difference]: Without dead ends: 75
[2025-04-28 21:21:42,601 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:42,601 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 4 mSDsluCounter, 42 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 78 SdHoareTripleChecker+Invalid, 46 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 44 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,601 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 78 Invalid, 46 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:42,602 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 75 states.
[2025-04-28 21:21:42,606 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 75 to 65.
[2025-04-28 21:21:42,606 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 65 states, 28 states have (on average 1.4642857142857142) internal successors, (41), 37 states have internal predecessors, (41), 16 states have call successors, (16), 7 states have call predecessors, (16), 20 states have return successors, (51), 20 states have call predecessors, (51), 16 states have call successors, (51)
[2025-04-28 21:21:42,607 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 65 states to 65 states and 108 transitions.
[2025-04-28 21:21:42,607 INFO  L79                 Accepts]: Start accepts. Automaton has 65 states and 108 transitions. Word has length 29
[2025-04-28 21:21:42,607 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,607 INFO  L485      AbstractCegarLoop]: Abstraction has 65 states and 108 transitions.
[2025-04-28 21:21:42,607 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:42,608 INFO  L278                IsEmpty]: Start isEmpty. Operand 65 states and 108 transitions.
[2025-04-28 21:21:42,608 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:42,608 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,608 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 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:42,609 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-04-28 21:21:42,609 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,609 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,609 INFO  L85        PathProgramCache]: Analyzing trace with hash -1628406641, now seen corresponding path program 1 times
[2025-04-28 21:21:42,609 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,609 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1646274137]
[2025-04-28 21:21:42,609 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,609 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,614 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:42,621 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:42,621 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,621 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,919 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:42,920 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,920 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1646274137]
[2025-04-28 21:21:42,920 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1646274137] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,920 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1029914276]
[2025-04-28 21:21:42,920 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,920 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,922 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,924 INFO  L229       MonitoredProcess]: Starting monitored process 14 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:42,929 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,021 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:43,041 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:43,041 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,041 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,043 INFO  L256         TraceCheckSpWp]: Trace formula consists of 155 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,044 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,146 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:43,146 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,801 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 10 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:44,801 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1029914276] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,801 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,801 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 14] total 23
[2025-04-28 21:21:44,801 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1085069469]
[2025-04-28 21:21:44,801 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,802 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:44,802 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,803 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:44,803 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=75, Invalid=431, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:44,803 INFO  L87              Difference]: Start difference. First operand 65 states and 108 transitions. Second operand  has 23 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 22 states have internal predecessors, (24), 13 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (17), 9 states have call predecessors, (17), 13 states have call successors, (17)
[2025-04-28 21:21:45,341 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,341 INFO  L93              Difference]: Finished difference Result 123 states and 203 transitions.
[2025-04-28 21:21:45,342 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-04-28 21:21:45,342 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 22 states have internal predecessors, (24), 13 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (17), 9 states have call predecessors, (17), 13 states have call successors, (17) Word has length 29
[2025-04-28 21:21:45,342 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,344 INFO  L225             Difference]: With dead ends: 123
[2025-04-28 21:21:45,344 INFO  L226             Difference]: Without dead ends: 113
[2025-04-28 21:21:45,344 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 78 GetRequests, 46 SyntacticMatches, 4 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 148 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=122, Invalid=748, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:45,345 INFO  L437           NwaCegarLoop]: 32 mSDtfsCounter, 12 mSDsluCounter, 290 mSDsCounter, 0 mSdLazyCounter, 511 mSolverCounterSat, 33 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 322 SdHoareTripleChecker+Invalid, 544 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 33 IncrementalHoareTripleChecker+Valid, 511 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,345 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 322 Invalid, 544 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [33 Valid, 511 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:45,345 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-04-28 21:21:45,353 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 75.
[2025-04-28 21:21:45,353 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 75 states, 33 states have (on average 1.393939393939394) internal successors, (46), 42 states have internal predecessors, (46), 16 states have call successors, (16), 7 states have call predecessors, (16), 25 states have return successors, (66), 25 states have call predecessors, (66), 16 states have call successors, (66)
[2025-04-28 21:21:45,354 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 75 states to 75 states and 128 transitions.
[2025-04-28 21:21:45,354 INFO  L79                 Accepts]: Start accepts. Automaton has 75 states and 128 transitions. Word has length 29
[2025-04-28 21:21:45,354 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,355 INFO  L485      AbstractCegarLoop]: Abstraction has 75 states and 128 transitions.
[2025-04-28 21:21:45,355 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 22 states have internal predecessors, (24), 13 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (17), 9 states have call predecessors, (17), 13 states have call successors, (17)
[2025-04-28 21:21:45,355 INFO  L278                IsEmpty]: Start isEmpty. Operand 75 states and 128 transitions.
[2025-04-28 21:21:45,356 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:45,356 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,356 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,363 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Ended with exit code 0
[2025-04-28 21:21:45,560 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19,14 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,560 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,560 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,561 INFO  L85        PathProgramCache]: Analyzing trace with hash -1451796281, now seen corresponding path program 2 times
[2025-04-28 21:21:45,561 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,561 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1618437912]
[2025-04-28 21:21:45,561 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:45,561 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,566 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:45,573 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:45,574 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:45,574 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,740 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:45,740 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,740 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1618437912]
[2025-04-28 21:21:45,740 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1618437912] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,740 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1949189839]
[2025-04-28 21:21:45,741 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:45,741 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,743 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,745 INFO  L229       MonitoredProcess]: Starting monitored process 15 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:45,748 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,864 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:45,885 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:45,885 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:45,885 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,886 INFO  L256         TraceCheckSpWp]: Trace formula consists of 163 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,887 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,088 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 2 proven. 11 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:46,088 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,672 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 2 proven. 12 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:47,673 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1949189839] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,673 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,673 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 13, 14] total 26
[2025-04-28 21:21:47,673 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1896827125]
[2025-04-28 21:21:47,673 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,674 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:47,674 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,674 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:47,674 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=76, Invalid=574, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:47,675 INFO  L87              Difference]: Start difference. First operand 75 states and 128 transitions. Second operand  has 26 states, 12 states have (on average 2.4166666666666665) internal successors, (29), 26 states have internal predecessors, (29), 15 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (19), 10 states have call predecessors, (19), 15 states have call successors, (19)
[2025-04-28 21:21:48,336 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,337 INFO  L93              Difference]: Finished difference Result 137 states and 225 transitions.
[2025-04-28 21:21:48,337 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 22 states. 
[2025-04-28 21:21:48,337 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 12 states have (on average 2.4166666666666665) internal successors, (29), 26 states have internal predecessors, (29), 15 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (19), 10 states have call predecessors, (19), 15 states have call successors, (19) Word has length 29
[2025-04-28 21:21:48,337 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,339 INFO  L225             Difference]: With dead ends: 137
[2025-04-28 21:21:48,339 INFO  L226             Difference]: Without dead ends: 116
[2025-04-28 21:21:48,340 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 86 GetRequests, 42 SyntacticMatches, 4 SemanticMatches, 40 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 264 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=243, Invalid=1479, Unknown=0, NotChecked=0, Total=1722
[2025-04-28 21:21:48,344 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 13 mSDsluCounter, 340 mSDsCounter, 0 mSdLazyCounter, 388 mSolverCounterSat, 51 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 369 SdHoareTripleChecker+Invalid, 439 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 51 IncrementalHoareTripleChecker+Valid, 388 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,344 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 369 Invalid, 439 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [51 Valid, 388 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:48,349 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 116 states.
[2025-04-28 21:21:48,365 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 116 to 64.
[2025-04-28 21:21:48,365 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 64 states, 29 states have (on average 1.3103448275862069) internal successors, (38), 35 states have internal predecessors, (38), 12 states have call successors, (12), 6 states have call predecessors, (12), 22 states have return successors, (58), 22 states have call predecessors, (58), 12 states have call successors, (58)
[2025-04-28 21:21:48,368 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 64 states to 64 states and 108 transitions.
[2025-04-28 21:21:48,368 INFO  L79                 Accepts]: Start accepts. Automaton has 64 states and 108 transitions. Word has length 29
[2025-04-28 21:21:48,368 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,368 INFO  L485      AbstractCegarLoop]: Abstraction has 64 states and 108 transitions.
[2025-04-28 21:21:48,369 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 12 states have (on average 2.4166666666666665) internal successors, (29), 26 states have internal predecessors, (29), 15 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (19), 10 states have call predecessors, (19), 15 states have call successors, (19)
[2025-04-28 21:21:48,369 INFO  L278                IsEmpty]: Start isEmpty. Operand 64 states and 108 transitions.
[2025-04-28 21:21:48,370 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:48,370 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,371 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,378 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Ended with exit code 0
[2025-04-28 21:21:48,571 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20,15 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,571 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,572 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,572 INFO  L85        PathProgramCache]: Analyzing trace with hash 1498027066, now seen corresponding path program 2 times
[2025-04-28 21:21:48,572 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,572 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1135750075]
[2025-04-28 21:21:48,572 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:48,572 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,577 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:48,585 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:48,585 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,585 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,745 INFO  L134       CoverageAnalysis]: Checked inductivity of 22 backedges. 12 proven. 3 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:48,745 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,745 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1135750075]
[2025-04-28 21:21:48,745 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1135750075] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:48,745 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1781105286]
[2025-04-28 21:21:48,746 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:48,746 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,748 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,750 INFO  L229       MonitoredProcess]: Starting monitored process 16 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:48,754 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (16)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,879 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:48,903 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:48,903 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,903 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,904 INFO  L256         TraceCheckSpWp]: Trace formula consists of 155 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,906 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
