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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:27,146 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:27,266 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0901174c-8aef-4869-ab0b-cb19ee9ed942/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:27,278 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:27,279 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:27,311 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:27,311 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:27,312 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:27,312 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:27,312 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:27,313 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:27,313 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:27,313 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:27,313 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:27,314 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:27,314 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:27,314 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:27,314 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:27,314 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:27,315 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:27,315 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:27,315 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:27,315 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:27,315 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:27,315 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:27,316 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:27,317 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:27,712 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:27,726 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:27,729 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:27,733 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:27,734 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:27,735 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0901174c-8aef-4869-ab0b-cb19ee9ed942/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-166.smt2
[2025-04-28 21:21:27,738 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:27,747 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:28,108 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0901174c-8aef-4869-ab0b-cb19ee9ed942/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-166.smt2
[2025-04-28 21:21:28,115 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:28,117 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:28,118 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:28,118 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:28,118 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:28,125 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,170 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28 Unit
[2025-04-28 21:21:28,170 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:28,172 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:28,172 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:28,172 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:28,191 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,191 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,227 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,227 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,231 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,236 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,240 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,241 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,242 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,259 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:28,260 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:28,261 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:28,261 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:28,262 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,266 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:28,288 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,307 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:28,311 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:28,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:28,332 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:28,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:28,332 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure END_QUERY given in one single declaration
[2025-04-28 21:21:28,332 INFO  L130     BoogieDeclarations]: Found specification of procedure END_QUERY
[2025-04-28 21:21:28,332 INFO  L138     BoogieDeclarations]: Found implementation of procedure END_QUERY
[2025-04-28 21:21:28,333 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_4 given in one single declaration
[2025-04-28 21:21:28,333 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_4
[2025-04-28 21:21:28,333 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_4
[2025-04-28 21:21:28,333 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_3 given in one single declaration
[2025-04-28 21:21:28,333 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_3
[2025-04-28 21:21:28,333 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_3
[2025-04-28 21:21:28,333 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_2 given in one single declaration
[2025-04-28 21:21:28,333 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_2
[2025-04-28 21:21:28,333 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_2
[2025-04-28 21:21:28,333 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:28,334 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:28,334 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:28,334 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:28,334 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:28,334 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:28,398 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:28,401 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:28,642 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:28,642 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:28,656 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:28,657 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:28,657 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:28 BoogieIcfgContainer
[2025-04-28 21:21:28,657 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:28,661 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:28,661 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:28,665 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:28,666 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:28" (1/3) ...
[2025-04-28 21:21:28,667 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@420bb45e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:28, skipping insertion in model container
[2025-04-28 21:21:28,667 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (2/3) ...
[2025-04-28 21:21:28,667 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@420bb45e and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:28, skipping insertion in model container
[2025-04-28 21:21:28,667 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:28" (3/3) ...
[2025-04-28 21:21:28,669 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:28,687 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:28,691 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 39 locations, 80 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:28,751 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:28,767 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;@33845fdf, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:28,767 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:28,772 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 39 states, 13 states have (on average 2.0) internal successors, (26), 26 states have internal predecessors, (26), 18 states have call successors, (18), 6 states have call predecessors, (18), 6 states have return successors, (18), 7 states have call predecessors, (18), 18 states have call successors, (18)
[2025-04-28 21:21:28,784 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:28,785 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,787 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,788 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,794 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,797 INFO  L85        PathProgramCache]: Analyzing trace with hash -1448264027, now seen corresponding path program 1 times
[2025-04-28 21:21:28,808 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,809 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [148907929]
[2025-04-28 21:21:28,809 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,811 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,851 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:28,883 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:28,883 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,884 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,294 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:29,295 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,295 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [148907929]
[2025-04-28 21:21:29,296 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [148907929] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,296 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:29,300 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:29,302 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [46264598]
[2025-04-28 21:21:29,304 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,310 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:29,310 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,357 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:29,359 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:29,362 INFO  L87              Difference]: Start difference. First operand  has 39 states, 13 states have (on average 2.0) internal successors, (26), 26 states have internal predecessors, (26), 18 states have call successors, (18), 6 states have call predecessors, (18), 6 states have return successors, (18), 7 states have call predecessors, (18), 18 states have call successors, (18) Second operand  has 7 states, 6 states have (on average 2.0) internal successors, (12), 7 states have internal predecessors, (12), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:29,700 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,703 INFO  L93              Difference]: Finished difference Result 45 states and 79 transitions.
[2025-04-28 21:21:29,705 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:29,707 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 2.0) internal successors, (12), 7 states have internal predecessors, (12), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 24
[2025-04-28 21:21:29,707 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,750 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:21:29,750 INFO  L226             Difference]: Without dead ends: 45
[2025-04-28 21:21:29,753 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:29,760 INFO  L437           NwaCegarLoop]: 45 mSDtfsCounter, 1 mSDsluCounter, 196 mSDsCounter, 0 mSdLazyCounter, 115 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 241 SdHoareTripleChecker+Invalid, 115 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 115 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,761 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 241 Invalid, 115 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 115 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:29,782 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 45 states.
[2025-04-28 21:21:29,848 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 45 to 45.
[2025-04-28 21:21:29,853 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 45 states, 16 states have (on average 1.75) internal successors, (28), 28 states have internal predecessors, (28), 18 states have call successors, (18), 6 states have call predecessors, (18), 10 states have return successors, (33), 10 states have call predecessors, (33), 18 states have call successors, (33)
[2025-04-28 21:21:29,862 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 45 states to 45 states and 79 transitions.
[2025-04-28 21:21:29,865 INFO  L79                 Accepts]: Start accepts. Automaton has 45 states and 79 transitions. Word has length 24
[2025-04-28 21:21:29,866 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,868 INFO  L485      AbstractCegarLoop]: Abstraction has 45 states and 79 transitions.
[2025-04-28 21:21:29,868 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 2.0) internal successors, (12), 7 states have internal predecessors, (12), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:29,869 INFO  L278                IsEmpty]: Start isEmpty. Operand 45 states and 79 transitions.
[2025-04-28 21:21:29,873 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:29,875 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,876 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:29,876 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:29,876 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,878 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,879 INFO  L85        PathProgramCache]: Analyzing trace with hash 2105987215, now seen corresponding path program 1 times
[2025-04-28 21:21:29,879 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,879 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1675092370]
[2025-04-28 21:21:29,879 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,880 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,924 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:29,969 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:29,972 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,973 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,253 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:30,253 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,253 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1675092370]
[2025-04-28 21:21:30,253 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1675092370] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,253 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1180204421]
[2025-04-28 21:21:30,254 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,254 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,257 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,262 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:30,265 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:30,329 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:30,366 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:30,366 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,366 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,368 INFO  L256         TraceCheckSpWp]: Trace formula consists of 122 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:30,377 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,478 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:30,479 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:31,331 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:31,331 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1180204421] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:31,331 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:31,332 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 9
[2025-04-28 21:21:31,332 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [369836091]
[2025-04-28 21:21:31,332 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,333 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:31,333 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,334 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:31,334 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:31,334 INFO  L87              Difference]: Start difference. First operand 45 states and 79 transitions. Second operand  has 9 states, 6 states have (on average 2.5) internal successors, (15), 9 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:31,572 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,572 INFO  L93              Difference]: Finished difference Result 53 states and 98 transitions.
[2025-04-28 21:21:31,572 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:31,573 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.5) internal successors, (15), 9 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8) Word has length 28
[2025-04-28 21:21:31,573 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,575 INFO  L225             Difference]: With dead ends: 53
[2025-04-28 21:21:31,575 INFO  L226             Difference]: Without dead ends: 53
[2025-04-28 21:21:31,575 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 64 GetRequests, 50 SyntacticMatches, 6 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=22, Invalid=68, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:31,576 INFO  L437           NwaCegarLoop]: 59 mSDtfsCounter, 2 mSDsluCounter, 300 mSDsCounter, 0 mSdLazyCounter, 132 mSolverCounterSat, 14 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 359 SdHoareTripleChecker+Invalid, 146 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 14 IncrementalHoareTripleChecker+Valid, 132 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,577 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 359 Invalid, 146 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [14 Valid, 132 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:31,578 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 53 states.
[2025-04-28 21:21:31,589 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 53 to 51.
[2025-04-28 21:21:31,590 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 51 states, 19 states have (on average 1.631578947368421) internal successors, (31), 31 states have internal predecessors, (31), 18 states have call successors, (18), 6 states have call predecessors, (18), 13 states have return successors, (44), 13 states have call predecessors, (44), 18 states have call successors, (44)
[2025-04-28 21:21:31,591 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 51 states to 51 states and 93 transitions.
[2025-04-28 21:21:31,592 INFO  L79                 Accepts]: Start accepts. Automaton has 51 states and 93 transitions. Word has length 28
[2025-04-28 21:21:31,592 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,592 INFO  L485      AbstractCegarLoop]: Abstraction has 51 states and 93 transitions.
[2025-04-28 21:21:31,592 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.5) internal successors, (15), 9 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:31,592 INFO  L278                IsEmpty]: Start isEmpty. Operand 51 states and 93 transitions.
[2025-04-28 21:21:31,594 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:31,594 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,595 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,601 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:31,799 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:31,799 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,800 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,800 INFO  L85        PathProgramCache]: Analyzing trace with hash -1095963254, now seen corresponding path program 1 times
[2025-04-28 21:21:31,800 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,800 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1464651941]
[2025-04-28 21:21:31,800 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,800 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,806 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:31,814 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:31,815 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,815 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,911 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:31,911 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,912 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1464651941]
[2025-04-28 21:21:31,912 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1464651941] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:31,912 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:31,912 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:31,912 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [737913907]
[2025-04-28 21:21:31,912 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,913 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:31,913 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,913 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:31,913 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:31,914 INFO  L87              Difference]: Start difference. First operand 51 states and 93 transitions. Second operand  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:32,156 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,156 INFO  L93              Difference]: Finished difference Result 75 states and 152 transitions.
[2025-04-28 21:21:32,157 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:32,157 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 28
[2025-04-28 21:21:32,158 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,160 INFO  L225             Difference]: With dead ends: 75
[2025-04-28 21:21:32,160 INFO  L226             Difference]: Without dead ends: 75
[2025-04-28 21:21:32,161 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=24, Invalid=48, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:32,162 INFO  L437           NwaCegarLoop]: 59 mSDtfsCounter, 6 mSDsluCounter, 186 mSDsCounter, 0 mSdLazyCounter, 116 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 245 SdHoareTripleChecker+Invalid, 125 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 116 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,162 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 245 Invalid, 125 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 116 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:32,163 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 75 states.
[2025-04-28 21:21:32,196 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 75 to 65.
[2025-04-28 21:21:32,200 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 65 states, 25 states have (on average 1.6) internal successors, (40), 39 states have internal predecessors, (40), 21 states have call successors, (21), 7 states have call predecessors, (21), 18 states have return successors, (67), 18 states have call predecessors, (67), 21 states have call successors, (67)
[2025-04-28 21:21:32,202 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 65 states to 65 states and 128 transitions.
[2025-04-28 21:21:32,203 INFO  L79                 Accepts]: Start accepts. Automaton has 65 states and 128 transitions. Word has length 28
[2025-04-28 21:21:32,203 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,203 INFO  L485      AbstractCegarLoop]: Abstraction has 65 states and 128 transitions.
[2025-04-28 21:21:32,203 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:32,203 INFO  L278                IsEmpty]: Start isEmpty. Operand 65 states and 128 transitions.
[2025-04-28 21:21:32,206 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:32,206 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,206 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,206 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:32,207 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,207 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,207 INFO  L85        PathProgramCache]: Analyzing trace with hash 268804103, now seen corresponding path program 1 times
[2025-04-28 21:21:32,207 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,207 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [424676272]
[2025-04-28 21:21:32,208 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,208 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,214 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:32,224 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:32,224 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,224 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,377 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:32,377 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,378 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [424676272]
[2025-04-28 21:21:32,378 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [424676272] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:32,378 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [933315844]
[2025-04-28 21:21:32,378 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,378 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,381 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:32,384 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:32,388 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:32,441 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:32,463 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:32,464 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,464 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,465 INFO  L256         TraceCheckSpWp]: Trace formula consists of 122 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:32,467 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,523 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:32,523 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,269 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:33,270 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [933315844] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,270 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,270 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 9
[2025-04-28 21:21:33,270 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1937877825]
[2025-04-28 21:21:33,270 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,271 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:33,271 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,271 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:33,272 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:33,272 INFO  L87              Difference]: Start difference. First operand 65 states and 128 transitions. Second operand  has 9 states, 6 states have (on average 2.5) internal successors, (15), 9 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:33,537 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,537 INFO  L93              Difference]: Finished difference Result 91 states and 195 transitions.
[2025-04-28 21:21:33,537 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:33,538 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.5) internal successors, (15), 9 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8) Word has length 28
[2025-04-28 21:21:33,538 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,541 INFO  L225             Difference]: With dead ends: 91
[2025-04-28 21:21:33,541 INFO  L226             Difference]: Without dead ends: 91
[2025-04-28 21:21:33,541 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 64 GetRequests, 51 SyntacticMatches, 5 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=22, Invalid=68, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:33,542 INFO  L437           NwaCegarLoop]: 59 mSDtfsCounter, 3 mSDsluCounter, 354 mSDsCounter, 0 mSdLazyCounter, 158 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 413 SdHoareTripleChecker+Invalid, 169 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 158 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,542 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 413 Invalid, 169 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 158 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:33,544 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-04-28 21:21:33,572 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 85.
[2025-04-28 21:21:33,574 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 85 states, 35 states have (on average 1.4285714285714286) internal successors, (50), 49 states have internal predecessors, (50), 21 states have call successors, (21), 7 states have call predecessors, (21), 28 states have return successors, (109), 28 states have call predecessors, (109), 21 states have call successors, (109)
[2025-04-28 21:21:33,576 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 85 states to 85 states and 180 transitions.
[2025-04-28 21:21:33,576 INFO  L79                 Accepts]: Start accepts. Automaton has 85 states and 180 transitions. Word has length 28
[2025-04-28 21:21:33,577 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,577 INFO  L485      AbstractCegarLoop]: Abstraction has 85 states and 180 transitions.
[2025-04-28 21:21:33,577 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.5) internal successors, (15), 9 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:33,577 INFO  L278                IsEmpty]: Start isEmpty. Operand 85 states and 180 transitions.
[2025-04-28 21:21:33,581 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:33,582 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,582 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,589 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:33,782 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,783 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,783 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,783 INFO  L85        PathProgramCache]: Analyzing trace with hash -1848427382, now seen corresponding path program 1 times
[2025-04-28 21:21:33,783 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,783 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1177124953]
[2025-04-28 21:21:33,783 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,783 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,788 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:33,798 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:33,799 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,799 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,983 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:33,983 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,983 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1177124953]
[2025-04-28 21:21:33,983 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1177124953] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,983 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,984 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:33,984 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1930012607]
[2025-04-28 21:21:33,984 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,984 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:33,984 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,985 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:33,985 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:33,985 INFO  L87              Difference]: Start difference. First operand 85 states and 180 transitions. Second operand  has 8 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:34,351 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,355 INFO  L93              Difference]: Finished difference Result 165 states and 388 transitions.
[2025-04-28 21:21:34,355 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:34,355 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7) Word has length 28
[2025-04-28 21:21:34,356 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,364 INFO  L225             Difference]: With dead ends: 165
[2025-04-28 21:21:34,366 INFO  L226             Difference]: Without dead ends: 165
[2025-04-28 21:21:34,367 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=100, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:34,368 INFO  L437           NwaCegarLoop]: 53 mSDtfsCounter, 8 mSDsluCounter, 249 mSDsCounter, 0 mSdLazyCounter, 233 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 302 SdHoareTripleChecker+Invalid, 249 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 233 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,370 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 302 Invalid, 249 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 233 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:34,371 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 165 states.
[2025-04-28 21:21:34,424 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 165 to 125.
[2025-04-28 21:21:34,425 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 54 states have (on average 1.3333333333333333) internal successors, (72), 70 states have internal predecessors, (72), 24 states have call successors, (24), 8 states have call predecessors, (24), 46 states have return successors, (196), 46 states have call predecessors, (196), 24 states have call successors, (196)
[2025-04-28 21:21:34,428 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 292 transitions.
[2025-04-28 21:21:34,428 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 292 transitions. Word has length 28
[2025-04-28 21:21:34,428 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,428 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 292 transitions.
[2025-04-28 21:21:34,429 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.8) internal successors, (14), 8 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:34,429 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 292 transitions.
[2025-04-28 21:21:34,434 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:34,435 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,436 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,436 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:34,436 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,437 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,438 INFO  L85        PathProgramCache]: Analyzing trace with hash -277755345, now seen corresponding path program 1 times
[2025-04-28 21:21:34,438 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,438 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1785585600]
[2025-04-28 21:21:34,441 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,441 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,449 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:34,459 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:34,459 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,459 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,577 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:34,577 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,577 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1785585600]
[2025-04-28 21:21:34,577 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1785585600] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,577 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1868195494]
[2025-04-28 21:21:34,577 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,577 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,581 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,583 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:34,587 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,645 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:34,669 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:34,669 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,670 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,671 INFO  L256         TraceCheckSpWp]: Trace formula consists of 126 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,672 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,708 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:34,708 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:35,216 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:35,216 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1868195494] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:35,217 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:35,217 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 8
[2025-04-28 21:21:35,217 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1676402326]
[2025-04-28 21:21:35,217 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,218 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:35,218 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,218 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:35,219 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:35,219 INFO  L87              Difference]: Start difference. First operand 125 states and 292 transitions. Second operand  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:35,380 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,380 INFO  L93              Difference]: Finished difference Result 203 states and 459 transitions.
[2025-04-28 21:21:35,380 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:35,381 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8) Word has length 28
[2025-04-28 21:21:35,381 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,385 INFO  L225             Difference]: With dead ends: 203
[2025-04-28 21:21:35,385 INFO  L226             Difference]: Without dead ends: 203
[2025-04-28 21:21:35,385 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 63 GetRequests, 52 SyntacticMatches, 4 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=20, Invalid=52, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:35,386 INFO  L437           NwaCegarLoop]: 57 mSDtfsCounter, 4 mSDsluCounter, 245 mSDsCounter, 0 mSdLazyCounter, 96 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 302 SdHoareTripleChecker+Invalid, 105 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 96 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,387 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 302 Invalid, 105 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 96 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:35,388 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 203 states.
[2025-04-28 21:21:35,446 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 203 to 133.
[2025-04-28 21:21:35,447 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 133 states, 58 states have (on average 1.3103448275862069) internal successors, (76), 74 states have internal predecessors, (76), 24 states have call successors, (24), 8 states have call predecessors, (24), 50 states have return successors, (209), 50 states have call predecessors, (209), 24 states have call successors, (209)
[2025-04-28 21:21:35,449 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 133 states to 133 states and 309 transitions.
[2025-04-28 21:21:35,449 INFO  L79                 Accepts]: Start accepts. Automaton has 133 states and 309 transitions. Word has length 28
[2025-04-28 21:21:35,450 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,450 INFO  L485      AbstractCegarLoop]: Abstraction has 133 states and 309 transitions.
[2025-04-28 21:21:35,450 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:35,450 INFO  L278                IsEmpty]: Start isEmpty. Operand 133 states and 309 transitions.
[2025-04-28 21:21:35,453 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:35,453 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,453 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,459 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:35,657 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:35,657 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,658 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,658 INFO  L85        PathProgramCache]: Analyzing trace with hash 1853855471, now seen corresponding path program 1 times
[2025-04-28 21:21:35,658 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,658 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1312983505]
[2025-04-28 21:21:35,658 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,658 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,664 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:35,671 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:35,671 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,671 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,737 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:35,737 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,737 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1312983505]
[2025-04-28 21:21:35,737 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1312983505] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,737 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:35,738 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:35,738 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1743524341]
[2025-04-28 21:21:35,738 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,738 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:35,738 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,739 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:35,739 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:35,739 INFO  L87              Difference]: Start difference. First operand 133 states and 309 transitions. Second operand  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:35,910 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,910 INFO  L93              Difference]: Finished difference Result 153 states and 327 transitions.
[2025-04-28 21:21:35,911 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:35,911 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 28
[2025-04-28 21:21:35,912 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,914 INFO  L225             Difference]: With dead ends: 153
[2025-04-28 21:21:35,914 INFO  L226             Difference]: Without dead ends: 145
[2025-04-28 21:21:35,914 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:35,916 INFO  L437           NwaCegarLoop]: 61 mSDtfsCounter, 6 mSDsluCounter, 194 mSDsCounter, 0 mSdLazyCounter, 95 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 255 SdHoareTripleChecker+Invalid, 106 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 95 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,916 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 255 Invalid, 106 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 95 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:35,917 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 145 states.
[2025-04-28 21:21:35,944 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 145 to 117.
[2025-04-28 21:21:35,944 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 117 states, 50 states have (on average 1.36) internal successors, (68), 66 states have internal predecessors, (68), 24 states have call successors, (24), 8 states have call predecessors, (24), 42 states have return successors, (167), 42 states have call predecessors, (167), 24 states have call successors, (167)
[2025-04-28 21:21:35,946 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 117 states to 117 states and 259 transitions.
[2025-04-28 21:21:35,946 INFO  L79                 Accepts]: Start accepts. Automaton has 117 states and 259 transitions. Word has length 28
[2025-04-28 21:21:35,949 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,949 INFO  L485      AbstractCegarLoop]: Abstraction has 117 states and 259 transitions.
[2025-04-28 21:21:35,949 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.5) internal successors, (14), 6 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:35,949 INFO  L278                IsEmpty]: Start isEmpty. Operand 117 states and 259 transitions.
[2025-04-28 21:21:35,952 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:35,952 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,953 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,953 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:35,953 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,953 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,953 INFO  L85        PathProgramCache]: Analyzing trace with hash 1292916692, now seen corresponding path program 1 times
[2025-04-28 21:21:35,954 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,954 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [91204002]
[2025-04-28 21:21:35,954 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,954 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,960 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:35,971 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:35,971 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,971 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,071 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:36,072 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,072 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [91204002]
[2025-04-28 21:21:36,072 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [91204002] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,072 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1242669923]
[2025-04-28 21:21:36,072 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,072 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,076 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,078 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:36,085 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,141 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:36,166 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:36,167 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,167 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,168 INFO  L256         TraceCheckSpWp]: Trace formula consists of 122 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,169 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,202 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:36,202 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:36,684 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:36,684 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1242669923] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:36,684 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:36,684 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 8
[2025-04-28 21:21:36,684 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [226031884]
[2025-04-28 21:21:36,684 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,685 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:36,685 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,685 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:36,685 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:36,685 INFO  L87              Difference]: Start difference. First operand 117 states and 259 transitions. Second operand  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:36,828 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,828 INFO  L93              Difference]: Finished difference Result 147 states and 312 transitions.
[2025-04-28 21:21:36,829 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:36,830 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8) Word has length 28
[2025-04-28 21:21:36,830 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,832 INFO  L225             Difference]: With dead ends: 147
[2025-04-28 21:21:36,832 INFO  L226             Difference]: Without dead ends: 143
[2025-04-28 21:21:36,833 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 63 GetRequests, 52 SyntacticMatches, 4 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=20, Invalid=52, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:36,833 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 4 mSDsluCounter, 194 mSDsCounter, 0 mSdLazyCounter, 79 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 250 SdHoareTripleChecker+Invalid, 91 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 79 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,834 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 250 Invalid, 91 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 79 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,834 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 143 states.
[2025-04-28 21:21:36,859 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 143 to 105.
[2025-04-28 21:21:36,859 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 44 states have (on average 1.4090909090909092) internal successors, (62), 60 states have internal predecessors, (62), 24 states have call successors, (24), 8 states have call predecessors, (24), 36 states have return successors, (143), 36 states have call predecessors, (143), 24 states have call successors, (143)
[2025-04-28 21:21:36,861 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 229 transitions.
[2025-04-28 21:21:36,861 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 229 transitions. Word has length 28
[2025-04-28 21:21:36,863 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,863 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 229 transitions.
[2025-04-28 21:21:36,863 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 3.0) internal successors, (15), 8 states have internal predecessors, (15), 5 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:36,863 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 229 transitions.
[2025-04-28 21:21:36,865 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:36,866 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,866 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,874 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:37,067 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,067 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,068 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,068 INFO  L85        PathProgramCache]: Analyzing trace with hash 508706900, now seen corresponding path program 1 times
[2025-04-28 21:21:37,068 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,068 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [758520515]
[2025-04-28 21:21:37,068 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,068 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,072 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:37,079 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:37,082 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,082 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,156 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:37,156 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,156 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [758520515]
[2025-04-28 21:21:37,157 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [758520515] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,157 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:37,157 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:37,157 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [799792910]
[2025-04-28 21:21:37,157 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,157 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:37,157 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,158 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:37,158 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:37,158 INFO  L87              Difference]: Start difference. First operand 105 states and 229 transitions. Second operand  has 7 states, 5 states have (on average 2.8) internal successors, (14), 7 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:37,425 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,425 INFO  L93              Difference]: Finished difference Result 160 states and 391 transitions.
[2025-04-28 21:21:37,426 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:37,426 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.8) internal successors, (14), 7 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 28
[2025-04-28 21:21:37,427 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,429 INFO  L225             Difference]: With dead ends: 160
[2025-04-28 21:21:37,429 INFO  L226             Difference]: Without dead ends: 130
[2025-04-28 21:21:37,430 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=19, Invalid=53, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:37,430 INFO  L437           NwaCegarLoop]: 64 mSDtfsCounter, 11 mSDsluCounter, 239 mSDsCounter, 0 mSdLazyCounter, 173 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 303 SdHoareTripleChecker+Invalid, 194 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 173 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,430 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 303 Invalid, 194 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 173 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:37,431 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 130 states.
[2025-04-28 21:21:37,450 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 130 to 118.
[2025-04-28 21:21:37,451 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 118 states, 48 states have (on average 1.5208333333333333) internal successors, (73), 69 states have internal predecessors, (73), 32 states have call successors, (32), 11 states have call predecessors, (32), 37 states have return successors, (138), 37 states have call predecessors, (138), 32 states have call successors, (138)
[2025-04-28 21:21:37,454 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 118 states to 118 states and 243 transitions.
[2025-04-28 21:21:37,454 INFO  L79                 Accepts]: Start accepts. Automaton has 118 states and 243 transitions. Word has length 28
[2025-04-28 21:21:37,454 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,455 INFO  L485      AbstractCegarLoop]: Abstraction has 118 states and 243 transitions.
[2025-04-28 21:21:37,456 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.8) internal successors, (14), 7 states have internal predecessors, (14), 4 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:37,456 INFO  L278                IsEmpty]: Start isEmpty. Operand 118 states and 243 transitions.
[2025-04-28 21:21:37,459 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:37,459 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,459 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,460 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:37,460 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,460 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,460 INFO  L85        PathProgramCache]: Analyzing trace with hash -1632663287, now seen corresponding path program 1 times
[2025-04-28 21:21:37,461 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,461 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2004478712]
[2025-04-28 21:21:37,461 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,461 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,466 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:37,470 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:37,470 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,470 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,608 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:37,608 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,608 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2004478712]
[2025-04-28 21:21:37,608 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2004478712] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,608 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:37,608 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:37,609 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1879398660]
[2025-04-28 21:21:37,609 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,609 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:37,609 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,609 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:37,609 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:37,610 INFO  L87              Difference]: Start difference. First operand 118 states and 243 transitions. Second operand  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:37,823 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,823 INFO  L93              Difference]: Finished difference Result 134 states and 279 transitions.
[2025-04-28 21:21:37,824 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:37,824 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7) Word has length 28
[2025-04-28 21:21:37,824 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,830 INFO  L225             Difference]: With dead ends: 134
[2025-04-28 21:21:37,830 INFO  L226             Difference]: Without dead ends: 132
[2025-04-28 21:21:37,830 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:37,831 INFO  L437           NwaCegarLoop]: 59 mSDtfsCounter, 2 mSDsluCounter, 304 mSDsCounter, 0 mSdLazyCounter, 168 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 363 SdHoareTripleChecker+Invalid, 169 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 168 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,831 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 363 Invalid, 169 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 168 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:37,832 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-04-28 21:21:37,851 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 124.
[2025-04-28 21:21:37,851 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 124 states, 51 states have (on average 1.4901960784313726) internal successors, (76), 72 states have internal predecessors, (76), 32 states have call successors, (32), 11 states have call predecessors, (32), 40 states have return successors, (153), 40 states have call predecessors, (153), 32 states have call successors, (153)
[2025-04-28 21:21:37,856 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 124 states to 124 states and 261 transitions.
[2025-04-28 21:21:37,856 INFO  L79                 Accepts]: Start accepts. Automaton has 124 states and 261 transitions. Word has length 28
[2025-04-28 21:21:37,858 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,858 INFO  L485      AbstractCegarLoop]: Abstraction has 124 states and 261 transitions.
[2025-04-28 21:21:37,858 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:37,858 INFO  L278                IsEmpty]: Start isEmpty. Operand 124 states and 261 transitions.
[2025-04-28 21:21:37,861 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:37,861 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,862 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,862 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:37,862 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,862 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,863 INFO  L85        PathProgramCache]: Analyzing trace with hash 652088659, now seen corresponding path program 1 times
[2025-04-28 21:21:37,863 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,863 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [524887214]
[2025-04-28 21:21:37,863 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,863 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,870 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:37,873 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:37,875 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,875 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,990 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:37,990 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,990 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [524887214]
[2025-04-28 21:21:37,990 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [524887214] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,991 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:37,991 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:37,991 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2007007775]
[2025-04-28 21:21:37,991 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,991 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:37,991 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,992 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:37,992 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:37,992 INFO  L87              Difference]: Start difference. First operand 124 states and 261 transitions. Second operand  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:38,174 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,174 INFO  L93              Difference]: Finished difference Result 138 states and 292 transitions.
[2025-04-28 21:21:38,175 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:38,175 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7) Word has length 28
[2025-04-28 21:21:38,175 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,178 INFO  L225             Difference]: With dead ends: 138
[2025-04-28 21:21:38,178 INFO  L226             Difference]: Without dead ends: 136
[2025-04-28 21:21:38,178 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:38,180 INFO  L437           NwaCegarLoop]: 58 mSDtfsCounter, 3 mSDsluCounter, 302 mSDsCounter, 0 mSdLazyCounter, 146 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 360 SdHoareTripleChecker+Invalid, 146 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 146 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,181 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 360 Invalid, 146 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 146 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:38,181 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 136 states.
[2025-04-28 21:21:38,201 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 136 to 126.
[2025-04-28 21:21:38,202 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 126 states, 52 states have (on average 1.4807692307692308) internal successors, (77), 73 states have internal predecessors, (77), 32 states have call successors, (32), 11 states have call predecessors, (32), 41 states have return successors, (157), 41 states have call predecessors, (157), 32 states have call successors, (157)
[2025-04-28 21:21:38,203 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 126 states to 126 states and 266 transitions.
[2025-04-28 21:21:38,203 INFO  L79                 Accepts]: Start accepts. Automaton has 126 states and 266 transitions. Word has length 28
[2025-04-28 21:21:38,204 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,204 INFO  L485      AbstractCegarLoop]: Abstraction has 126 states and 266 transitions.
[2025-04-28 21:21:38,204 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:38,204 INFO  L278                IsEmpty]: Start isEmpty. Operand 126 states and 266 transitions.
[2025-04-28 21:21:38,206 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:38,206 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,206 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,206 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:38,206 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,207 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,207 INFO  L85        PathProgramCache]: Analyzing trace with hash 1657196334, now seen corresponding path program 1 times
[2025-04-28 21:21:38,207 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,208 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1395518304]
[2025-04-28 21:21:38,208 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,208 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,212 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:38,215 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:38,215 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,215 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,307 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:38,307 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,307 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1395518304]
[2025-04-28 21:21:38,307 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1395518304] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:38,307 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,307 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:38,307 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1641289480]
[2025-04-28 21:21:38,308 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,308 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:38,308 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,308 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:38,308 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:38,309 INFO  L87              Difference]: Start difference. First operand 126 states and 266 transitions. Second operand  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:38,516 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,516 INFO  L93              Difference]: Finished difference Result 136 states and 283 transitions.
[2025-04-28 21:21:38,517 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:38,517 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7) Word has length 28
[2025-04-28 21:21:38,517 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,519 INFO  L225             Difference]: With dead ends: 136
[2025-04-28 21:21:38,520 INFO  L226             Difference]: Without dead ends: 134
[2025-04-28 21:21:38,520 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:38,522 INFO  L437           NwaCegarLoop]: 58 mSDtfsCounter, 2 mSDsluCounter, 296 mSDsCounter, 0 mSdLazyCounter, 161 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 354 SdHoareTripleChecker+Invalid, 163 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 161 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,522 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 354 Invalid, 163 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 161 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:38,524 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-04-28 21:21:38,537 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 122.
[2025-04-28 21:21:38,538 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 122 states, 50 states have (on average 1.5) internal successors, (75), 71 states have internal predecessors, (75), 32 states have call successors, (32), 11 states have call predecessors, (32), 39 states have return successors, (147), 39 states have call predecessors, (147), 32 states have call successors, (147)
[2025-04-28 21:21:38,540 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 122 states to 122 states and 254 transitions.
[2025-04-28 21:21:38,540 INFO  L79                 Accepts]: Start accepts. Automaton has 122 states and 254 transitions. Word has length 28
[2025-04-28 21:21:38,540 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,540 INFO  L485      AbstractCegarLoop]: Abstraction has 122 states and 254 transitions.
[2025-04-28 21:21:38,541 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 8 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:38,541 INFO  L278                IsEmpty]: Start isEmpty. Operand 122 states and 254 transitions.
[2025-04-28 21:21:38,542 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:38,542 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,543 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,543 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:38,543 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,543 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,543 INFO  L85        PathProgramCache]: Analyzing trace with hash -1799917090, now seen corresponding path program 1 times
[2025-04-28 21:21:38,544 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,544 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1750032169]
[2025-04-28 21:21:38,544 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,544 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,549 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:38,557 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:38,557 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,557 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,644 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:38,644 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,644 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1750032169]
[2025-04-28 21:21:38,644 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1750032169] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:38,644 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,644 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:38,645 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1619956917]
[2025-04-28 21:21:38,645 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,645 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:38,645 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,645 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:38,645 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:38,646 INFO  L87              Difference]: Start difference. First operand 122 states and 254 transitions. Second operand  has 7 states, 5 states have (on average 3.0) internal successors, (15), 7 states have internal predecessors, (15), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:38,877 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,877 INFO  L93              Difference]: Finished difference Result 173 states and 395 transitions.
[2025-04-28 21:21:38,877 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:38,878 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 3.0) internal successors, (15), 7 states have internal predecessors, (15), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8) Word has length 32
[2025-04-28 21:21:38,878 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,880 INFO  L225             Difference]: With dead ends: 173
[2025-04-28 21:21:38,880 INFO  L226             Difference]: Without dead ends: 149
[2025-04-28 21:21:38,881 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:38,882 INFO  L437           NwaCegarLoop]: 58 mSDtfsCounter, 9 mSDsluCounter, 225 mSDsCounter, 0 mSdLazyCounter, 174 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 283 SdHoareTripleChecker+Invalid, 186 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 174 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,883 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 283 Invalid, 186 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 174 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:38,884 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 149 states.
[2025-04-28 21:21:38,901 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 149 to 125.
[2025-04-28 21:21:38,902 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 125 states, 51 states have (on average 1.5098039215686274) internal successors, (77), 73 states have internal predecessors, (77), 34 states have call successors, (34), 12 states have call predecessors, (34), 39 states have return successors, (138), 39 states have call predecessors, (138), 34 states have call successors, (138)
[2025-04-28 21:21:38,904 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 125 states to 125 states and 249 transitions.
[2025-04-28 21:21:38,904 INFO  L79                 Accepts]: Start accepts. Automaton has 125 states and 249 transitions. Word has length 32
[2025-04-28 21:21:38,904 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,904 INFO  L485      AbstractCegarLoop]: Abstraction has 125 states and 249 transitions.
[2025-04-28 21:21:38,904 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 3.0) internal successors, (15), 7 states have internal predecessors, (15), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:38,904 INFO  L278                IsEmpty]: Start isEmpty. Operand 125 states and 249 transitions.
[2025-04-28 21:21:38,906 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:38,906 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,907 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,907 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:38,907 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,907 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,907 INFO  L85        PathProgramCache]: Analyzing trace with hash 225371235, now seen corresponding path program 1 times
[2025-04-28 21:21:38,908 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,908 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1618242661]
[2025-04-28 21:21:38,908 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,908 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,917 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:38,922 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:38,925 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,926 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,034 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:39,034 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,034 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1618242661]
[2025-04-28 21:21:39,034 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1618242661] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,034 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1974507905]
[2025-04-28 21:21:39,034 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,034 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,037 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,040 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:39,044 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,106 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:39,129 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:39,130 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,130 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,131 INFO  L256         TraceCheckSpWp]: Trace formula consists of 144 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,132 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,181 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:39,182 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,069 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:40,069 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1974507905] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,069 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,069 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 10
[2025-04-28 21:21:40,069 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1995018993]
[2025-04-28 21:21:40,069 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,070 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:40,070 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,070 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:40,071 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:40,071 INFO  L87              Difference]: Start difference. First operand 125 states and 249 transitions. Second operand  has 10 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 10 states have internal predecessors, (19), 6 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 5 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:21:40,323 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,323 INFO  L93              Difference]: Finished difference Result 161 states and 323 transitions.
[2025-04-28 21:21:40,323 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:40,324 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 10 states have internal predecessors, (19), 6 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 5 states have call predecessors, (11), 6 states have call successors, (11) Word has length 32
[2025-04-28 21:21:40,324 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,326 INFO  L225             Difference]: With dead ends: 161
[2025-04-28 21:21:40,326 INFO  L226             Difference]: Without dead ends: 153
[2025-04-28 21:21:40,327 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 73 GetRequests, 59 SyntacticMatches, 5 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=24, Invalid=86, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:40,327 INFO  L437           NwaCegarLoop]: 54 mSDtfsCounter, 8 mSDsluCounter, 269 mSDsCounter, 0 mSdLazyCounter, 175 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 323 SdHoareTripleChecker+Invalid, 193 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 175 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,328 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 323 Invalid, 193 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 175 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:40,329 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-04-28 21:21:40,340 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 121.
[2025-04-28 21:21:40,340 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 121 states, 48 states have (on average 1.6041666666666667) internal successors, (77), 72 states have internal predecessors, (77), 37 states have call successors, (37), 13 states have call predecessors, (37), 35 states have return successors, (122), 35 states have call predecessors, (122), 37 states have call successors, (122)
[2025-04-28 21:21:40,342 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 121 states to 121 states and 236 transitions.
[2025-04-28 21:21:40,342 INFO  L79                 Accepts]: Start accepts. Automaton has 121 states and 236 transitions. Word has length 32
[2025-04-28 21:21:40,342 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,342 INFO  L485      AbstractCegarLoop]: Abstraction has 121 states and 236 transitions.
[2025-04-28 21:21:40,343 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 10 states have internal predecessors, (19), 6 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (11), 5 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:21:40,343 INFO  L278                IsEmpty]: Start isEmpty. Operand 121 states and 236 transitions.
[2025-04-28 21:21:40,345 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:40,345 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,345 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,351 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:40,549 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,549 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,550 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,550 INFO  L85        PathProgramCache]: Analyzing trace with hash -1963391042, now seen corresponding path program 1 times
[2025-04-28 21:21:40,550 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,550 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [339746665]
[2025-04-28 21:21:40,551 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,551 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,557 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:40,568 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:40,569 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,569 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,026 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:41,026 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,026 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [339746665]
[2025-04-28 21:21:41,026 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [339746665] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,026 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [383010299]
[2025-04-28 21:21:41,026 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,026 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,029 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,032 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:41,035 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,099 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:41,120 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:41,121 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,121 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,122 INFO  L256         TraceCheckSpWp]: Trace formula consists of 140 conjuncts, 46 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,124 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,357 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:41,357 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,011 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:44,011 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [383010299] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,011 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,012 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 18
[2025-04-28 21:21:44,012 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1656106430]
[2025-04-28 21:21:44,012 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,012 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:44,012 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,013 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:44,014 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=264, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:44,015 INFO  L87              Difference]: Start difference. First operand 121 states and 236 transitions. Second operand  has 18 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 18 states have internal predecessors, (22), 10 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (14), 7 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:21:44,870 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,870 INFO  L93              Difference]: Finished difference Result 158 states and 315 transitions.
[2025-04-28 21:21:44,870 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:21:44,871 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 18 states have internal predecessors, (22), 10 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (14), 7 states have call predecessors, (14), 10 states have call successors, (14) Word has length 32
[2025-04-28 21:21:44,871 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,873 INFO  L225             Difference]: With dead ends: 158
[2025-04-28 21:21:44,873 INFO  L226             Difference]: Without dead ends: 158
[2025-04-28 21:21:44,874 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 80 GetRequests, 57 SyntacticMatches, 2 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 32 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=70, Invalid=436, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:44,874 INFO  L437           NwaCegarLoop]: 62 mSDtfsCounter, 16 mSDsluCounter, 548 mSDsCounter, 0 mSdLazyCounter, 548 mSolverCounterSat, 17 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 31 SdHoareTripleChecker+Valid, 610 SdHoareTripleChecker+Invalid, 565 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 17 IncrementalHoareTripleChecker+Valid, 548 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,874 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [31 Valid, 610 Invalid, 565 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [17 Valid, 548 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:44,875 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 158 states.
[2025-04-28 21:21:44,885 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 158 to 128.
[2025-04-28 21:21:44,886 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 128 states, 51 states have (on average 1.5686274509803921) internal successors, (80), 76 states have internal predecessors, (80), 38 states have call successors, (38), 13 states have call predecessors, (38), 38 states have return successors, (135), 38 states have call predecessors, (135), 38 states have call successors, (135)
[2025-04-28 21:21:44,887 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 128 states to 128 states and 253 transitions.
[2025-04-28 21:21:44,887 INFO  L79                 Accepts]: Start accepts. Automaton has 128 states and 253 transitions. Word has length 32
[2025-04-28 21:21:44,887 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,888 INFO  L485      AbstractCegarLoop]: Abstraction has 128 states and 253 transitions.
[2025-04-28 21:21:44,888 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 18 states have internal predecessors, (22), 10 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (14), 7 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:21:44,888 INFO  L278                IsEmpty]: Start isEmpty. Operand 128 states and 253 transitions.
[2025-04-28 21:21:44,890 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:44,890 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,890 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,895 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:45,090 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-04-28 21:21:45,091 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,091 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,091 INFO  L85        PathProgramCache]: Analyzing trace with hash -942524233, now seen corresponding path program 1 times
[2025-04-28 21:21:45,091 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,091 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1495784517]
[2025-04-28 21:21:45,091 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,091 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,096 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:45,100 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:45,100 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,101 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,230 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:45,230 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,230 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1495784517]
[2025-04-28 21:21:45,230 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1495784517] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,230 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,230 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:45,230 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1328542576]
[2025-04-28 21:21:45,230 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,231 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:45,231 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,231 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:45,231 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:45,232 INFO  L87              Difference]: Start difference. First operand 128 states and 253 transitions. Second operand  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:45,433 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,434 INFO  L93              Difference]: Finished difference Result 144 states and 287 transitions.
[2025-04-28 21:21:45,434 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:45,434 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8) Word has length 32
[2025-04-28 21:21:45,435 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,437 INFO  L225             Difference]: With dead ends: 144
[2025-04-28 21:21:45,437 INFO  L226             Difference]: Without dead ends: 142
[2025-04-28 21:21:45,438 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=25, Invalid=85, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:45,438 INFO  L437           NwaCegarLoop]: 53 mSDtfsCounter, 6 mSDsluCounter, 315 mSDsCounter, 0 mSdLazyCounter, 156 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 368 SdHoareTripleChecker+Invalid, 158 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 156 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,439 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 368 Invalid, 158 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 156 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:45,440 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-04-28 21:21:45,450 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 126.
[2025-04-28 21:21:45,451 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 126 states, 50 states have (on average 1.58) internal successors, (79), 75 states have internal predecessors, (79), 38 states have call successors, (38), 13 states have call predecessors, (38), 37 states have return successors, (131), 37 states have call predecessors, (131), 38 states have call successors, (131)
[2025-04-28 21:21:45,453 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 126 states to 126 states and 248 transitions.
[2025-04-28 21:21:45,453 INFO  L79                 Accepts]: Start accepts. Automaton has 126 states and 248 transitions. Word has length 32
[2025-04-28 21:21:45,453 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,453 INFO  L485      AbstractCegarLoop]: Abstraction has 126 states and 248 transitions.
[2025-04-28 21:21:45,453 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:45,454 INFO  L278                IsEmpty]: Start isEmpty. Operand 126 states and 248 transitions.
[2025-04-28 21:21:45,456 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:45,456 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,456 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,456 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:21:45,456 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,457 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,457 INFO  L85        PathProgramCache]: Analyzing trace with hash 1163680786, now seen corresponding path program 1 times
[2025-04-28 21:21:45,457 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,457 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1153081874]
[2025-04-28 21:21:45,457 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,457 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,462 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:45,466 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:45,466 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,466 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,589 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:45,589 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,589 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1153081874]
[2025-04-28 21:21:45,589 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1153081874] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,589 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,589 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:45,589 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [291466593]
[2025-04-28 21:21:45,589 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,590 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:45,590 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,591 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:45,591 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:45,591 INFO  L87              Difference]: Start difference. First operand 126 states and 248 transitions. Second operand  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:45,811 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,811 INFO  L93              Difference]: Finished difference Result 144 states and 284 transitions.
[2025-04-28 21:21:45,812 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:45,812 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8) Word has length 32
[2025-04-28 21:21:45,814 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,816 INFO  L225             Difference]: With dead ends: 144
[2025-04-28 21:21:45,816 INFO  L226             Difference]: Without dead ends: 142
[2025-04-28 21:21:45,816 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=20, Invalid=70, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:45,817 INFO  L437           NwaCegarLoop]: 60 mSDtfsCounter, 4 mSDsluCounter, 355 mSDsCounter, 0 mSdLazyCounter, 181 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 415 SdHoareTripleChecker+Invalid, 184 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 181 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,817 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 415 Invalid, 184 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 181 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:45,819 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 142 states.
[2025-04-28 21:21:45,830 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 142 to 130.
[2025-04-28 21:21:45,830 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 130 states, 52 states have (on average 1.5576923076923077) internal successors, (81), 77 states have internal predecessors, (81), 38 states have call successors, (38), 13 states have call predecessors, (38), 39 states have return successors, (139), 39 states have call predecessors, (139), 38 states have call successors, (139)
[2025-04-28 21:21:45,832 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 130 states to 130 states and 258 transitions.
[2025-04-28 21:21:45,833 INFO  L79                 Accepts]: Start accepts. Automaton has 130 states and 258 transitions. Word has length 32
[2025-04-28 21:21:45,833 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,833 INFO  L485      AbstractCegarLoop]: Abstraction has 130 states and 258 transitions.
[2025-04-28 21:21:45,833 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:45,834 INFO  L278                IsEmpty]: Start isEmpty. Operand 130 states and 258 transitions.
[2025-04-28 21:21:45,837 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:45,837 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,838 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,838 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:21:45,838 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,838 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,838 INFO  L85        PathProgramCache]: Analyzing trace with hash -551020562, now seen corresponding path program 1 times
[2025-04-28 21:21:45,838 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,838 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1496835721]
[2025-04-28 21:21:45,839 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,839 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,843 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:45,869 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:45,869 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,869 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,075 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:46,075 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,075 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1496835721]
[2025-04-28 21:21:46,075 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1496835721] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,075 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [325215902]
[2025-04-28 21:21:46,075 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,075 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,078 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,080 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:46,085 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,156 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:46,175 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:46,175 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,175 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,178 INFO  L256         TraceCheckSpWp]: Trace formula consists of 144 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,180 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,266 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:46,266 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,789 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:46,789 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [325215902] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,789 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,789 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 7, 7] total 18
[2025-04-28 21:21:46,790 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [542612790]
[2025-04-28 21:21:46,790 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,790 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:46,790 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,791 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:46,791 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=266, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:46,791 INFO  L87              Difference]: Start difference. First operand 130 states and 258 transitions. Second operand  has 18 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 18 states have internal predecessors, (27), 9 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (16), 10 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:47,381 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,381 INFO  L93              Difference]: Finished difference Result 226 states and 459 transitions.
[2025-04-28 21:21:47,381 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 21 states. 
[2025-04-28 21:21:47,382 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 18 states have internal predecessors, (27), 9 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (16), 10 states have call predecessors, (16), 9 states have call successors, (16) Word has length 32
[2025-04-28 21:21:47,382 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,385 INFO  L225             Difference]: With dead ends: 226
[2025-04-28 21:21:47,385 INFO  L226             Difference]: Without dead ends: 186
[2025-04-28 21:21:47,385 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 84 GetRequests, 57 SyntacticMatches, 4 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 38 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=79, Invalid=521, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:47,386 INFO  L437           NwaCegarLoop]: 52 mSDtfsCounter, 14 mSDsluCounter, 564 mSDsCounter, 0 mSdLazyCounter, 447 mSolverCounterSat, 42 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 27 SdHoareTripleChecker+Valid, 616 SdHoareTripleChecker+Invalid, 489 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 42 IncrementalHoareTripleChecker+Valid, 447 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,386 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [27 Valid, 616 Invalid, 489 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [42 Valid, 447 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:47,387 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 186 states.
[2025-04-28 21:21:47,403 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 186 to 138.
[2025-04-28 21:21:47,404 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 138 states, 56 states have (on average 1.5178571428571428) internal successors, (85), 81 states have internal predecessors, (85), 38 states have call successors, (38), 13 states have call predecessors, (38), 43 states have return successors, (154), 43 states have call predecessors, (154), 38 states have call successors, (154)
[2025-04-28 21:21:47,405 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 138 states to 138 states and 277 transitions.
[2025-04-28 21:21:47,406 INFO  L79                 Accepts]: Start accepts. Automaton has 138 states and 277 transitions. Word has length 32
[2025-04-28 21:21:47,406 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,406 INFO  L485      AbstractCegarLoop]: Abstraction has 138 states and 277 transitions.
[2025-04-28 21:21:47,406 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 11 states have (on average 2.4545454545454546) internal successors, (27), 18 states have internal predecessors, (27), 9 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (16), 10 states have call predecessors, (16), 9 states have call successors, (16)
[2025-04-28 21:21:47,406 INFO  L278                IsEmpty]: Start isEmpty. Operand 138 states and 277 transitions.
[2025-04-28 21:21:47,408 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:47,409 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,409 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,415 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:47,613 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,613 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,613 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,613 INFO  L85        PathProgramCache]: Analyzing trace with hash 2082012636, now seen corresponding path program 1 times
[2025-04-28 21:21:47,614 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,614 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [247239940]
[2025-04-28 21:21:47,614 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,614 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,618 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:21:47,622 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:47,623 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,623 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,761 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:47,761 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,761 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [247239940]
[2025-04-28 21:21:47,761 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [247239940] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,761 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,761 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:47,762 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1622665929]
[2025-04-28 21:21:47,762 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,763 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:47,763 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,764 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:47,764 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=56, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:47,765 INFO  L87              Difference]: Start difference. First operand 138 states and 277 transitions. Second operand  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:47,970 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,970 INFO  L93              Difference]: Finished difference Result 170 states and 349 transitions.
[2025-04-28 21:21:47,971 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:47,971 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8) Word has length 32
[2025-04-28 21:21:47,971 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,974 INFO  L225             Difference]: With dead ends: 170
[2025-04-28 21:21:47,974 INFO  L226             Difference]: Without dead ends: 166
[2025-04-28 21:21:47,975 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=26, Invalid=84, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:47,975 INFO  L437           NwaCegarLoop]: 52 mSDtfsCounter, 6 mSDsluCounter, 266 mSDsCounter, 0 mSdLazyCounter, 132 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 318 SdHoareTripleChecker+Invalid, 136 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 132 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,975 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 318 Invalid, 136 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 132 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:47,976 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 166 states.
[2025-04-28 21:21:47,992 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 166 to 142.
[2025-04-28 21:21:47,995 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 58 states have (on average 1.5) internal successors, (87), 83 states have internal predecessors, (87), 38 states have call successors, (38), 13 states have call predecessors, (38), 45 states have return successors, (162), 45 states have call predecessors, (162), 38 states have call successors, (162)
[2025-04-28 21:21:47,997 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 287 transitions.
[2025-04-28 21:21:47,997 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 287 transitions. Word has length 32
[2025-04-28 21:21:47,997 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,997 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 287 transitions.
[2025-04-28 21:21:47,997 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:47,998 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 287 transitions.
[2025-04-28 21:21:48,000 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:48,000 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,000 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,001 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-04-28 21:21:48,001 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,001 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,001 INFO  L85        PathProgramCache]: Analyzing trace with hash 425735981, now seen corresponding path program 2 times
[2025-04-28 21:21:48,001 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,002 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1305341925]
[2025-04-28 21:21:48,002 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:48,002 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,009 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 36 statements into 2 equivalence classes.
[2025-04-28 21:21:48,014 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:48,015 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,015 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,089 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:48,089 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,089 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1305341925]
[2025-04-28 21:21:48,089 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1305341925] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:48,089 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2121233147]
[2025-04-28 21:21:48,089 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:48,089 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,092 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,094 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:48,098 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,166 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 36 statements into 2 equivalence classes.
[2025-04-28 21:21:48,185 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:48,185 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,185 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,186 INFO  L256         TraceCheckSpWp]: Trace formula consists of 158 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,188 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,220 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:48,220 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,803 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:48,803 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2121233147] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,803 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,804 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 9
[2025-04-28 21:21:48,804 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [562374499]
[2025-04-28 21:21:48,804 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,804 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:48,804 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,805 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:48,805 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:48,805 INFO  L87              Difference]: Start difference. First operand 142 states and 287 transitions. Second operand  has 9 states, 5 states have (on average 3.8) internal successors, (19), 9 states have internal predecessors, (19), 6 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:21:48,963 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,963 INFO  L93              Difference]: Finished difference Result 170 states and 336 transitions.
[2025-04-28 21:21:48,964 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:48,964 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 3.8) internal successors, (19), 9 states have internal predecessors, (19), 6 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 6 states have call successors, (11) Word has length 36
[2025-04-28 21:21:48,964 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,966 INFO  L225             Difference]: With dead ends: 170
[2025-04-28 21:21:48,967 INFO  L226             Difference]: Without dead ends: 164
[2025-04-28 21:21:48,967 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 83 GetRequests, 67 SyntacticMatches, 5 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 13 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=52, Invalid=104, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:48,968 INFO  L437           NwaCegarLoop]: 56 mSDtfsCounter, 10 mSDsluCounter, 225 mSDsCounter, 0 mSdLazyCounter, 97 mSolverCounterSat, 38 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 281 SdHoareTripleChecker+Invalid, 135 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 38 IncrementalHoareTripleChecker+Valid, 97 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,968 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 281 Invalid, 135 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [38 Valid, 97 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:48,968 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 164 states.
[2025-04-28 21:21:48,981 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 164 to 146.
[2025-04-28 21:21:48,981 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 146 states, 60 states have (on average 1.4833333333333334) internal successors, (89), 85 states have internal predecessors, (89), 38 states have call successors, (38), 13 states have call predecessors, (38), 47 states have return successors, (169), 47 states have call predecessors, (169), 38 states have call successors, (169)
[2025-04-28 21:21:48,983 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 146 states to 146 states and 296 transitions.
[2025-04-28 21:21:48,983 INFO  L79                 Accepts]: Start accepts. Automaton has 146 states and 296 transitions. Word has length 36
[2025-04-28 21:21:48,983 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,983 INFO  L485      AbstractCegarLoop]: Abstraction has 146 states and 296 transitions.
[2025-04-28 21:21:48,983 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 3.8) internal successors, (19), 9 states have internal predecessors, (19), 6 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:21:48,984 INFO  L278                IsEmpty]: Start isEmpty. Operand 146 states and 296 transitions.
[2025-04-28 21:21:48,986 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:48,986 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,986 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,992 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:49,186 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20,9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,187 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,188 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,188 INFO  L85        PathProgramCache]: Analyzing trace with hash 1049528392, now seen corresponding path program 1 times
[2025-04-28 21:21:49,188 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,188 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [113014503]
[2025-04-28 21:21:49,188 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,188 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,193 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:49,201 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:49,201 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,202 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,302 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:49,302 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,302 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [113014503]
[2025-04-28 21:21:49,302 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [113014503] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,302 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,303 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:49,303 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1366785443]
[2025-04-28 21:21:49,303 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,303 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:49,303 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,304 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:49,304 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:49,304 INFO  L87              Difference]: Start difference. First operand 146 states and 296 transitions. Second operand  has 8 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:49,576 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,576 INFO  L93              Difference]: Finished difference Result 219 states and 482 transitions.
[2025-04-28 21:21:49,576 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:49,577 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:49,577 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,580 INFO  L225             Difference]: With dead ends: 219
[2025-04-28 21:21:49,580 INFO  L226             Difference]: Without dead ends: 195
[2025-04-28 21:21:49,580 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:49,581 INFO  L437           NwaCegarLoop]: 63 mSDtfsCounter, 12 mSDsluCounter, 294 mSDsCounter, 0 mSdLazyCounter, 263 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 357 SdHoareTripleChecker+Invalid, 281 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 263 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,581 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 357 Invalid, 281 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 263 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:49,582 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 195 states.
[2025-04-28 21:21:49,609 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 195 to 157.
[2025-04-28 21:21:49,610 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 157 states, 65 states have (on average 1.4615384615384615) internal successors, (95), 91 states have internal predecessors, (95), 40 states have call successors, (40), 14 states have call predecessors, (40), 51 states have return successors, (164), 51 states have call predecessors, (164), 40 states have call successors, (164)
[2025-04-28 21:21:49,611 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 157 states to 157 states and 299 transitions.
[2025-04-28 21:21:49,611 INFO  L79                 Accepts]: Start accepts. Automaton has 157 states and 299 transitions. Word has length 36
[2025-04-28 21:21:49,611 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,611 INFO  L485      AbstractCegarLoop]: Abstraction has 157 states and 299 transitions.
[2025-04-28 21:21:49,611 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:49,611 INFO  L278                IsEmpty]: Start isEmpty. Operand 157 states and 299 transitions.
[2025-04-28 21:21:49,615 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:49,615 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,615 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,615 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-04-28 21:21:49,615 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,616 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,616 INFO  L85        PathProgramCache]: Analyzing trace with hash 1857186496, now seen corresponding path program 1 times
[2025-04-28 21:21:49,616 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,616 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [236986204]
[2025-04-28 21:21:49,616 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,617 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,623 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:49,629 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:49,632 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,632 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,710 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:49,710 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,710 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [236986204]
[2025-04-28 21:21:49,710 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [236986204] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,710 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,710 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:49,711 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1231627619]
[2025-04-28 21:21:49,711 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,711 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:49,711 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,712 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:49,712 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:49,712 INFO  L87              Difference]: Start difference. First operand 157 states and 299 transitions. Second operand  has 8 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:49,924 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,924 INFO  L93              Difference]: Finished difference Result 177 states and 329 transitions.
[2025-04-28 21:21:49,927 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:49,927 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9) Word has length 36
[2025-04-28 21:21:49,927 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,929 INFO  L225             Difference]: With dead ends: 177
[2025-04-28 21:21:49,929 INFO  L226             Difference]: Without dead ends: 161
[2025-04-28 21:21:49,929 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:49,930 INFO  L437           NwaCegarLoop]: 58 mSDtfsCounter, 9 mSDsluCounter, 277 mSDsCounter, 0 mSdLazyCounter, 211 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 335 SdHoareTripleChecker+Invalid, 222 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 211 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,931 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 335 Invalid, 222 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 211 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:49,931 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 161 states.
[2025-04-28 21:21:49,942 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 161 to 151.
[2025-04-28 21:21:49,943 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 151 states, 62 states have (on average 1.4838709677419355) internal successors, (92), 88 states have internal predecessors, (92), 40 states have call successors, (40), 14 states have call predecessors, (40), 48 states have return successors, (153), 48 states have call predecessors, (153), 40 states have call successors, (153)
[2025-04-28 21:21:49,944 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 151 states to 151 states and 285 transitions.
[2025-04-28 21:21:49,944 INFO  L79                 Accepts]: Start accepts. Automaton has 151 states and 285 transitions. Word has length 36
[2025-04-28 21:21:49,944 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,944 INFO  L485      AbstractCegarLoop]: Abstraction has 151 states and 285 transitions.
[2025-04-28 21:21:49,945 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 8 states have internal predecessors, (16), 3 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:49,945 INFO  L278                IsEmpty]: Start isEmpty. Operand 151 states and 285 transitions.
[2025-04-28 21:21:49,947 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:49,947 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,947 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,947 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-04-28 21:21:49,947 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,948 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,948 INFO  L85        PathProgramCache]: Analyzing trace with hash -758323678, now seen corresponding path program 1 times
[2025-04-28 21:21:49,948 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,948 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1763027373]
[2025-04-28 21:21:49,948 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,949 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,954 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:49,961 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:49,961 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,961 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,079 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:50,080 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,080 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1763027373]
[2025-04-28 21:21:50,080 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1763027373] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,080 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2057370223]
[2025-04-28 21:21:50,080 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,080 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,083 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,085 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:50,088 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,162 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:50,184 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:50,184 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,184 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,185 INFO  L256         TraceCheckSpWp]: Trace formula consists of 162 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,186 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,235 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:50,237 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,978 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:51,978 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2057370223] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,978 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,978 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 11] total 13
[2025-04-28 21:21:51,978 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2097403895]
[2025-04-28 21:21:51,978 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,979 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:51,979 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,979 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:51,979 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=127, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:51,980 INFO  L87              Difference]: Start difference. First operand 151 states and 285 transitions. Second operand  has 13 states, 8 states have (on average 2.375) internal successors, (19), 13 states have internal predecessors, (19), 6 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 6 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:21:52,337 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,338 INFO  L93              Difference]: Finished difference Result 225 states and 421 transitions.
[2025-04-28 21:21:52,338 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:52,338 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 8 states have (on average 2.375) internal successors, (19), 13 states have internal predecessors, (19), 6 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 6 states have call predecessors, (11), 6 states have call successors, (11) Word has length 36
[2025-04-28 21:21:52,339 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,341 INFO  L225             Difference]: With dead ends: 225
[2025-04-28 21:21:52,341 INFO  L226             Difference]: Without dead ends: 199
[2025-04-28 21:21:52,342 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 85 GetRequests, 63 SyntacticMatches, 9 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 12 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=39, Invalid=171, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:52,342 INFO  L437           NwaCegarLoop]: 61 mSDtfsCounter, 4 mSDsluCounter, 452 mSDsCounter, 0 mSdLazyCounter, 310 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 513 SdHoareTripleChecker+Invalid, 332 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 310 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,343 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 513 Invalid, 332 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 310 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:52,344 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 199 states.
[2025-04-28 21:21:52,359 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 199 to 169.
[2025-04-28 21:21:52,361 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 169 states, 71 states have (on average 1.4225352112676057) internal successors, (101), 97 states have internal predecessors, (101), 40 states have call successors, (40), 14 states have call predecessors, (40), 57 states have return successors, (166), 57 states have call predecessors, (166), 40 states have call successors, (166)
[2025-04-28 21:21:52,363 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 169 states to 169 states and 307 transitions.
[2025-04-28 21:21:52,363 INFO  L79                 Accepts]: Start accepts. Automaton has 169 states and 307 transitions. Word has length 36
[2025-04-28 21:21:52,364 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,364 INFO  L485      AbstractCegarLoop]: Abstraction has 169 states and 307 transitions.
[2025-04-28 21:21:52,364 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 8 states have (on average 2.375) internal successors, (19), 13 states have internal predecessors, (19), 6 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 6 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:21:52,364 INFO  L278                IsEmpty]: Start isEmpty. Operand 169 states and 307 transitions.
[2025-04-28 21:21:52,366 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:52,367 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,367 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,374 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:21:52,568 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable23
[2025-04-28 21:21:52,568 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,569 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,569 INFO  L85        PathProgramCache]: Analyzing trace with hash -1300152192, now seen corresponding path program 1 times
[2025-04-28 21:21:52,569 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,569 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [189382306]
[2025-04-28 21:21:52,569 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,569 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,575 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:52,578 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:52,578 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,579 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,713 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:52,713 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,714 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [189382306]
[2025-04-28 21:21:52,714 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [189382306] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,714 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,714 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [] total 10
[2025-04-28 21:21:52,715 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1651781326]
[2025-04-28 21:21:52,715 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,716 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:52,716 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,716 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:52,716 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=72, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:52,717 INFO  L87              Difference]: Start difference. First operand 169 states and 307 transitions. Second operand  has 10 states, 6 states have (on average 2.5) internal successors, (15), 10 states have internal predecessors, (15), 5 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:52,890 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,891 INFO  L93              Difference]: Finished difference Result 183 states and 338 transitions.
[2025-04-28 21:21:52,891 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:52,891 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.5) internal successors, (15), 10 states have internal predecessors, (15), 5 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 5 states have call successors, (9) Word has length 36
[2025-04-28 21:21:52,891 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,892 INFO  L225             Difference]: With dead ends: 183
[2025-04-28 21:21:52,892 INFO  L226             Difference]: Without dead ends: 178
[2025-04-28 21:21:52,893 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 15 GetRequests, 5 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=30, Invalid=102, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:52,893 INFO  L437           NwaCegarLoop]: 57 mSDtfsCounter, 4 mSDsluCounter, 331 mSDsCounter, 0 mSdLazyCounter, 164 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 388 SdHoareTripleChecker+Invalid, 168 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 164 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,893 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 388 Invalid, 168 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 164 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:52,894 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 178 states.
[2025-04-28 21:21:52,904 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 178 to 158.
[2025-04-28 21:21:52,904 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 158 states, 66 states have (on average 1.4393939393939394) internal successors, (95), 91 states have internal predecessors, (95), 39 states have call successors, (39), 14 states have call predecessors, (39), 52 states have return successors, (146), 52 states have call predecessors, (146), 39 states have call successors, (146)
[2025-04-28 21:21:52,906 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 158 states to 158 states and 280 transitions.
[2025-04-28 21:21:52,906 INFO  L79                 Accepts]: Start accepts. Automaton has 158 states and 280 transitions. Word has length 36
[2025-04-28 21:21:52,906 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,906 INFO  L485      AbstractCegarLoop]: Abstraction has 158 states and 280 transitions.
[2025-04-28 21:21:52,906 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.5) internal successors, (15), 10 states have internal predecessors, (15), 5 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 5 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:52,906 INFO  L278                IsEmpty]: Start isEmpty. Operand 158 states and 280 transitions.
[2025-04-28 21:21:52,908 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:52,908 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,908 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,908 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable24
[2025-04-28 21:21:52,908 INFO  L403      AbstractCegarLoop]: === Iteration 25 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,909 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,909 INFO  L85        PathProgramCache]: Analyzing trace with hash 1577646760, now seen corresponding path program 3 times
[2025-04-28 21:21:52,909 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,909 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1053638543]
[2025-04-28 21:21:52,909 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:52,909 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,914 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 36 statements into 3 equivalence classes.
[2025-04-28 21:21:52,920 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:52,921 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:52,921 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,033 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:53,033 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,034 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1053638543]
[2025-04-28 21:21:53,034 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1053638543] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,034 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1449008521]
[2025-04-28 21:21:53,034 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:53,034 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,036 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,039 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:53,043 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,144 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 36 statements into 3 equivalence classes.
[2025-04-28 21:21:53,168 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:53,168 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:53,169 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,170 INFO  L256         TraceCheckSpWp]: Trace formula consists of 162 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,172 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,222 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:53,223 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,370 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:54,370 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1449008521] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,370 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,370 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 15
[2025-04-28 21:21:54,370 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [811042073]
[2025-04-28 21:21:54,370 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,371 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:54,371 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,371 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:54,371 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=173, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:54,372 INFO  L87              Difference]: Start difference. First operand 158 states and 280 transitions. Second operand  has 15 states, 7 states have (on average 3.142857142857143) internal successors, (22), 15 states have internal predecessors, (22), 10 states have call successors, (13), 1 states have call predecessors, (13), 7 states have return successors, (15), 6 states have call predecessors, (15), 10 states have call successors, (15)
[2025-04-28 21:21:54,621 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,621 INFO  L93              Difference]: Finished difference Result 208 states and 389 transitions.
[2025-04-28 21:21:54,622 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:54,622 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 3.142857142857143) internal successors, (22), 15 states have internal predecessors, (22), 10 states have call successors, (13), 1 states have call predecessors, (13), 7 states have return successors, (15), 6 states have call predecessors, (15), 10 states have call successors, (15) Word has length 36
[2025-04-28 21:21:54,622 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,624 INFO  L225             Difference]: With dead ends: 208
[2025-04-28 21:21:54,624 INFO  L226             Difference]: Without dead ends: 200
[2025-04-28 21:21:54,624 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 85 GetRequests, 64 SyntacticMatches, 4 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 40 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=71, Invalid=271, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:54,625 INFO  L437           NwaCegarLoop]: 51 mSDtfsCounter, 7 mSDsluCounter, 269 mSDsCounter, 0 mSdLazyCounter, 211 mSolverCounterSat, 39 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 320 SdHoareTripleChecker+Invalid, 250 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 39 IncrementalHoareTripleChecker+Valid, 211 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,625 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 320 Invalid, 250 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [39 Valid, 211 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:54,626 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 200 states.
[2025-04-28 21:21:54,638 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 200 to 166.
[2025-04-28 21:21:54,639 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 166 states, 70 states have (on average 1.4142857142857144) internal successors, (99), 95 states have internal predecessors, (99), 39 states have call successors, (39), 14 states have call predecessors, (39), 56 states have return successors, (159), 56 states have call predecessors, (159), 39 states have call successors, (159)
[2025-04-28 21:21:54,640 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 166 states to 166 states and 297 transitions.
[2025-04-28 21:21:54,640 INFO  L79                 Accepts]: Start accepts. Automaton has 166 states and 297 transitions. Word has length 36
[2025-04-28 21:21:54,640 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,641 INFO  L485      AbstractCegarLoop]: Abstraction has 166 states and 297 transitions.
[2025-04-28 21:21:54,641 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 3.142857142857143) internal successors, (22), 15 states have internal predecessors, (22), 10 states have call successors, (13), 1 states have call predecessors, (13), 7 states have return successors, (15), 6 states have call predecessors, (15), 10 states have call successors, (15)
[2025-04-28 21:21:54,641 INFO  L278                IsEmpty]: Start isEmpty. Operand 166 states and 297 transitions.
[2025-04-28 21:21:54,642 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:54,643 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,643 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,649 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:54,843 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable25,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,843 INFO  L403      AbstractCegarLoop]: === Iteration 26 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,844 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,844 INFO  L85        PathProgramCache]: Analyzing trace with hash 1290288492, now seen corresponding path program 1 times
[2025-04-28 21:21:54,844 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,844 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1188247813]
[2025-04-28 21:21:54,844 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,844 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,848 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:54,857 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:54,859 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,859 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,010 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:55,010 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,010 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1188247813]
[2025-04-28 21:21:55,010 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1188247813] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,010 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [331677846]
[2025-04-28 21:21:55,010 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,011 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,013 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,016 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:55,020 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,158 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:21:55,184 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:55,184 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,184 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,185 INFO  L256         TraceCheckSpWp]: Trace formula consists of 166 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,187 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,368 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:55,368 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
