./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-152.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:19,989 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:20,112 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0810e75e-2f66-482d-a6ab-8d2a1eb8c4da/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:20,119 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:20,120 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:20,159 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:20,160 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:20,160 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:20,162 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:20,162 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:20,164 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:20,164 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:20,164 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:20,165 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:20,165 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:20,165 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:20,166 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:20,166 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:20,166 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:20,166 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:20,166 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:20,166 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:20,167 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:20,167 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:20,167 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:20,168 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:20,168 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:20,584 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:20,595 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:20,599 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:20,601 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:20,602 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:20,604 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0810e75e-2f66-482d-a6ab-8d2a1eb8c4da/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-152.smt2
[2025-04-28 21:21:20,607 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:20,614 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:21,194 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0810e75e-2f66-482d-a6ab-8d2a1eb8c4da/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-152.smt2
[2025-04-28 21:21:21,199 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:21,201 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:21,202 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:21,203 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:21,203 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:21,207 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,258 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21 Unit
[2025-04-28 21:21:21,259 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:21,261 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:21,262 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:21,262 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:21,283 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,284 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,313 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,313 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,330 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,331 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,334 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,336 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,337 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,367 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:21,369 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:21,369 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:21,369 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:21,370 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (1/1) ...
[2025-04-28 21:21:21,373 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:21,388 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:21,404 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:21,408 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:21,421 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:21,421 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:21,421 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:21,421 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:21,421 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:21,421 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:21,421 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:21,421 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:21,422 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:21,422 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_0 given in one single declaration
[2025-04-28 21:21:21,422 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_0
[2025-04-28 21:21:21,422 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_0
[2025-04-28 21:21:21,422 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:21,422 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:21,422 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:21,536 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:21,538 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:22,116 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:22,118 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:22,135 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:22,135 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:22,136 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:22 BoogieIcfgContainer
[2025-04-28 21:21:22,136 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:22,139 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:22,139 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:22,143 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:22,144 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:21" (1/3) ...
[2025-04-28 21:21:22,144 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@836fbad and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:22, skipping insertion in model container
[2025-04-28 21:21:22,145 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:21" (2/3) ...
[2025-04-28 21:21:22,145 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@836fbad and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:22, skipping insertion in model container
[2025-04-28 21:21:22,145 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:22" (3/3) ...
[2025-04-28 21:21:22,146 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:22,166 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:22,169 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 5 procedures, 70 locations, 187 edges, 5 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:22,229 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:22,246 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;@3a440f5, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:22,246 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:22,251 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 70 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 22 states have internal predecessors, (22), 55 states have call successors, (55), 4 states have call predecessors, (55), 4 states have return successors, (55), 44 states have call predecessors, (55), 55 states have call successors, (55)
[2025-04-28 21:21:22,262 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:22,262 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,263 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:22,263 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,269 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,270 INFO  L85        PathProgramCache]: Analyzing trace with hash -923880869, now seen corresponding path program 1 times
[2025-04-28 21:21:22,279 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,279 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1642343757]
[2025-04-28 21:21:22,279 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,280 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,312 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:22,336 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:22,336 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,337 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,756 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:22,756 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,757 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1642343757]
[2025-04-28 21:21:22,758 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1642343757] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:22,758 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:22,764 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:22,766 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [249092363]
[2025-04-28 21:21:22,767 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:22,774 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:22,774 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:22,810 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:22,811 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:22,813 INFO  L87              Difference]: Start difference. First operand  has 70 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 22 states have internal predecessors, (22), 55 states have call successors, (55), 4 states have call predecessors, (55), 4 states have return successors, (55), 44 states have call predecessors, (55), 55 states have call successors, (55) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:23,069 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,069 INFO  L93              Difference]: Finished difference Result 72 states and 142 transitions.
[2025-04-28 21:21:23,073 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:23,075 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:23,075 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,088 INFO  L225             Difference]: With dead ends: 72
[2025-04-28 21:21:23,088 INFO  L226             Difference]: Without dead ends: 72
[2025-04-28 21:21:23,090 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:23,094 INFO  L437           NwaCegarLoop]: 123 mSDtfsCounter, 1 mSDsluCounter, 225 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 348 SdHoareTripleChecker+Invalid, 44 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 44 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,095 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 348 Invalid, 44 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:23,122 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 72 states.
[2025-04-28 21:21:23,204 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 72 to 70.
[2025-04-28 21:21:23,205 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 70 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 21 states have internal predecessors, (21), 55 states have call successors, (55), 4 states have call predecessors, (55), 5 states have return successors, (64), 44 states have call predecessors, (64), 55 states have call successors, (64)
[2025-04-28 21:21:23,219 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 140 transitions.
[2025-04-28 21:21:23,220 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 140 transitions. Word has length 12
[2025-04-28 21:21:23,221 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,221 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 140 transitions.
[2025-04-28 21:21:23,222 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:23,223 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 140 transitions.
[2025-04-28 21:21:23,225 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:23,225 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,225 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:23,226 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:23,226 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,227 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,227 INFO  L85        PathProgramCache]: Analyzing trace with hash -958467135, now seen corresponding path program 1 times
[2025-04-28 21:21:23,227 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,227 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [519620863]
[2025-04-28 21:21:23,227 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,227 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,232 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:23,235 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:23,235 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,235 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,453 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:23,453 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,453 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [519620863]
[2025-04-28 21:21:23,453 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [519620863] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:23,453 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:23,453 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:23,453 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1269119199]
[2025-04-28 21:21:23,453 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:23,456 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:23,456 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:23,457 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:23,457 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:23,458 INFO  L87              Difference]: Start difference. First operand 70 states and 140 transitions. Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:23,606 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,608 INFO  L93              Difference]: Finished difference Result 72 states and 141 transitions.
[2025-04-28 21:21:23,609 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:23,609 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:23,609 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,612 INFO  L225             Difference]: With dead ends: 72
[2025-04-28 21:21:23,613 INFO  L226             Difference]: Without dead ends: 72
[2025-04-28 21:21:23,613 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:23,614 INFO  L437           NwaCegarLoop]: 124 mSDtfsCounter, 1 mSDsluCounter, 227 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 351 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,614 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 351 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:23,615 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 72 states.
[2025-04-28 21:21:23,630 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 72 to 70.
[2025-04-28 21:21:23,630 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 70 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 21 states have internal predecessors, (21), 55 states have call successors, (55), 4 states have call predecessors, (55), 5 states have return successors, (63), 44 states have call predecessors, (63), 55 states have call successors, (63)
[2025-04-28 21:21:23,634 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 139 transitions.
[2025-04-28 21:21:23,635 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 139 transitions. Word has length 12
[2025-04-28 21:21:23,635 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,635 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 139 transitions.
[2025-04-28 21:21:23,635 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:23,635 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 139 transitions.
[2025-04-28 21:21:23,639 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:23,639 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,640 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:23,640 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:23,640 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,644 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,644 INFO  L85        PathProgramCache]: Analyzing trace with hash 805300230, now seen corresponding path program 1 times
[2025-04-28 21:21:23,644 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,644 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1561622625]
[2025-04-28 21:21:23,644 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,644 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,655 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:23,661 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:23,661 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,661 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,752 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:23,752 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,752 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1561622625]
[2025-04-28 21:21:23,752 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1561622625] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:23,753 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [904187769]
[2025-04-28 21:21:23,753 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,753 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:23,756 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:23,758 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:23,764 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:23,837 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:23,878 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:23,878 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,879 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,884 INFO  L256         TraceCheckSpWp]: Trace formula consists of 166 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:23,892 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:23,964 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 9 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:23,964 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:23,964 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [904187769] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:23,964 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:23,964 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 4
[2025-04-28 21:21:23,964 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1479184127]
[2025-04-28 21:21:23,964 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:23,966 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:23,966 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:23,966 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:23,967 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:23,967 INFO  L87              Difference]: Start difference. First operand 70 states and 139 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (6), 2 states have call predecessors, (6), 2 states have return successors, (6), 1 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:24,083 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:24,084 INFO  L93              Difference]: Finished difference Result 72 states and 140 transitions.
[2025-04-28 21:21:24,085 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:24,085 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (6), 2 states have call predecessors, (6), 2 states have return successors, (6), 1 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:24,085 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:24,088 INFO  L225             Difference]: With dead ends: 72
[2025-04-28 21:21:24,091 INFO  L226             Difference]: Without dead ends: 72
[2025-04-28 21:21:24,092 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 27 GetRequests, 25 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:24,094 INFO  L437           NwaCegarLoop]: 125 mSDtfsCounter, 1 mSDsluCounter, 229 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 354 SdHoareTripleChecker+Invalid, 35 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:24,095 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 354 Invalid, 35 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:24,096 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 72 states.
[2025-04-28 21:21:24,118 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 72 to 70.
[2025-04-28 21:21:24,120 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 70 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 21 states have internal predecessors, (21), 55 states have call successors, (55), 4 states have call predecessors, (55), 5 states have return successors, (62), 44 states have call predecessors, (62), 55 states have call successors, (62)
[2025-04-28 21:21:24,125 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 138 transitions.
[2025-04-28 21:21:24,125 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 138 transitions. Word has length 24
[2025-04-28 21:21:24,125 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:24,127 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 138 transitions.
[2025-04-28 21:21:24,127 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (6), 2 states have call predecessors, (6), 2 states have return successors, (6), 1 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:24,129 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 138 transitions.
[2025-04-28 21:21:24,131 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:24,134 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,135 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 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:24,142 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:24,335 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:24,336 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,336 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,336 INFO  L85        PathProgramCache]: Analyzing trace with hash -1083947660, now seen corresponding path program 1 times
[2025-04-28 21:21:24,336 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,336 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1049930168]
[2025-04-28 21:21:24,337 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,337 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,346 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:24,362 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:24,362 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,363 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,910 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 8 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:24,910 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,911 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1049930168]
[2025-04-28 21:21:24,911 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1049930168] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:24,912 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1114404784]
[2025-04-28 21:21:24,912 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,912 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:24,915 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:24,918 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:24,924 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:24,999 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:25,041 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:25,041 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,041 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,056 INFO  L256         TraceCheckSpWp]: Trace formula consists of 218 conjuncts, 85 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:25,059 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:25,719 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:25,719 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:28,411 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 10 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:28,411 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1114404784] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:28,411 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:28,411 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 11, 11] total 21
[2025-04-28 21:21:28,412 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [645781241]
[2025-04-28 21:21:28,412 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,412 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:28,412 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,413 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:28,414 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=67, Invalid=353, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:28,415 INFO  L87              Difference]: Start difference. First operand 70 states and 138 transitions. Second operand  has 21 states, 8 states have (on average 2.625) internal successors, (21), 14 states have internal predecessors, (21), 15 states have call successors, (17), 1 states have call predecessors, (17), 8 states have return successors, (17), 10 states have call predecessors, (17), 15 states have call successors, (17)
[2025-04-28 21:21:30,723 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,723 INFO  L93              Difference]: Finished difference Result 96 states and 410 transitions.
[2025-04-28 21:21:30,724 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:30,724 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 8 states have (on average 2.625) internal successors, (21), 14 states have internal predecessors, (21), 15 states have call successors, (17), 1 states have call predecessors, (17), 8 states have return successors, (17), 10 states have call predecessors, (17), 15 states have call successors, (17) Word has length 28
[2025-04-28 21:21:30,724 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,735 INFO  L225             Difference]: With dead ends: 96
[2025-04-28 21:21:30,735 INFO  L226             Difference]: Without dead ends: 96
[2025-04-28 21:21:30,735 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 70 GetRequests, 44 SyntacticMatches, 0 SemanticMatches, 26 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 65 ImplicationChecksByTransitivity, 1.0s TimeCoverageRelationStatistics Valid=136, Invalid=620, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:30,736 INFO  L437           NwaCegarLoop]: 90 mSDtfsCounter, 20 mSDsluCounter, 637 mSDsCounter, 0 mSdLazyCounter, 1164 mSolverCounterSat, 80 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 28 SdHoareTripleChecker+Valid, 727 SdHoareTripleChecker+Invalid, 1244 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 80 IncrementalHoareTripleChecker+Valid, 1164 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,736 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [28 Valid, 727 Invalid, 1244 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [80 Valid, 1164 Invalid, 0 Unknown, 0 Unchecked, 1.8s Time]
[2025-04-28 21:21:30,737 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 96 states.
[2025-04-28 21:21:30,816 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 96 to 82.
[2025-04-28 21:21:30,816 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 24 states have internal predecessors, (25), 62 states have call successors, (62), 5 states have call predecessors, (62), 7 states have return successors, (118), 52 states have call predecessors, (118), 62 states have call successors, (118)
[2025-04-28 21:21:30,822 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 205 transitions.
[2025-04-28 21:21:30,822 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 205 transitions. Word has length 28
[2025-04-28 21:21:30,822 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,822 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 205 transitions.
[2025-04-28 21:21:30,822 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 8 states have (on average 2.625) internal successors, (21), 14 states have internal predecessors, (21), 15 states have call successors, (17), 1 states have call predecessors, (17), 8 states have return successors, (17), 10 states have call predecessors, (17), 15 states have call successors, (17)
[2025-04-28 21:21:30,822 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 205 transitions.
[2025-04-28 21:21:30,828 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:21:30,828 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,828 INFO  L218           NwaCegarLoop]: trace histogram [8, 8, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,833 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:31,033 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:31,033 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,033 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,034 INFO  L85        PathProgramCache]: Analyzing trace with hash -1133161182, now seen corresponding path program 1 times
[2025-04-28 21:21:31,034 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,034 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1455810847]
[2025-04-28 21:21:31,034 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,034 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,043 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 48 statements into 1 equivalence classes.
[2025-04-28 21:21:31,060 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:31,060 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,060 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,562 INFO  L134       CoverageAnalysis]: Checked inductivity of 91 backedges. 10 proven. 22 refuted. 0 times theorem prover too weak. 59 trivial. 0 not checked.
[2025-04-28 21:21:31,562 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,562 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1455810847]
[2025-04-28 21:21:31,562 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1455810847] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,562 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [455042502]
[2025-04-28 21:21:31,562 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,563 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,565 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,567 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:31,571 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,652 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 48 statements into 1 equivalence classes.
[2025-04-28 21:21:31,719 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:31,719 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,720 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,725 INFO  L256         TraceCheckSpWp]: Trace formula consists of 434 conjuncts, 111 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,729 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,391 INFO  L134       CoverageAnalysis]: Checked inductivity of 91 backedges. 12 proven. 36 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:32,391 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:34,639 INFO  L134       CoverageAnalysis]: Checked inductivity of 91 backedges. 12 proven. 36 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:34,639 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [455042502] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:34,639 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:34,639 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 14, 13] total 26
[2025-04-28 21:21:34,639 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [386301400]
[2025-04-28 21:21:34,639 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,640 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:34,640 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,641 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:34,641 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=73, Invalid=577, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:34,642 INFO  L87              Difference]: Start difference. First operand 82 states and 205 transitions. Second operand  has 26 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 18 states have internal predecessors, (24), 22 states have call successors, (31), 1 states have call predecessors, (31), 9 states have return successors, (31), 16 states have call predecessors, (31), 22 states have call successors, (31)
[2025-04-28 21:21:38,112 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,113 INFO  L93              Difference]: Finished difference Result 117 states and 592 transitions.
[2025-04-28 21:21:38,113 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:21:38,113 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 18 states have internal predecessors, (24), 22 states have call successors, (31), 1 states have call predecessors, (31), 9 states have return successors, (31), 16 states have call predecessors, (31), 22 states have call successors, (31) Word has length 48
[2025-04-28 21:21:38,114 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,121 INFO  L225             Difference]: With dead ends: 117
[2025-04-28 21:21:38,122 INFO  L226             Difference]: Without dead ends: 117
[2025-04-28 21:21:38,122 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 118 GetRequests, 81 SyntacticMatches, 0 SemanticMatches, 37 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 124 ImplicationChecksByTransitivity, 1.4s TimeCoverageRelationStatistics Valid=233, Invalid=1249, Unknown=0, NotChecked=0, Total=1482
[2025-04-28 21:21:38,123 INFO  L437           NwaCegarLoop]: 86 mSDtfsCounter, 54 mSDsluCounter, 852 mSDsCounter, 0 mSdLazyCounter, 2100 mSolverCounterSat, 172 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 69 SdHoareTripleChecker+Valid, 938 SdHoareTripleChecker+Invalid, 2272 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 172 IncrementalHoareTripleChecker+Valid, 2100 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,123 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [69 Valid, 938 Invalid, 2272 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [172 Valid, 2100 Invalid, 0 Unknown, 0 Unchecked, 2.5s Time]
[2025-04-28 21:21:38,124 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-04-28 21:21:38,219 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 92.
[2025-04-28 21:21:38,220 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 15 states have (on average 1.8666666666666667) internal successors, (28), 27 states have internal predecessors, (28), 66 states have call successors, (66), 5 states have call predecessors, (66), 10 states have return successors, (270), 59 states have call predecessors, (270), 66 states have call successors, (270)
[2025-04-28 21:21:38,224 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 364 transitions.
[2025-04-28 21:21:38,224 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 364 transitions. Word has length 48
[2025-04-28 21:21:38,225 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,226 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 364 transitions.
[2025-04-28 21:21:38,228 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 18 states have internal predecessors, (24), 22 states have call successors, (31), 1 states have call predecessors, (31), 9 states have return successors, (31), 16 states have call predecessors, (31), 22 states have call successors, (31)
[2025-04-28 21:21:38,229 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 364 transitions.
[2025-04-28 21:21:38,231 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:21:38,234 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,235 INFO  L218           NwaCegarLoop]: trace histogram [8, 8, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,241 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:38,435 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,435 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,436 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,436 INFO  L85        PathProgramCache]: Analyzing trace with hash 1010714015, now seen corresponding path program 1 times
[2025-04-28 21:21:38,436 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,436 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [377439114]
[2025-04-28 21:21:38,436 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,436 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,445 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 48 statements into 1 equivalence classes.
[2025-04-28 21:21:38,478 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:38,478 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,478 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,803 INFO  L134       CoverageAnalysis]: Checked inductivity of 91 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 71 trivial. 0 not checked.
[2025-04-28 21:21:38,803 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,804 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [377439114]
[2025-04-28 21:21:38,804 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [377439114] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:38,804 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [936908]
[2025-04-28 21:21:38,805 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,805 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,807 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:38,809 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:38,814 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:38,900 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 48 statements into 1 equivalence classes.
[2025-04-28 21:21:38,969 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:38,969 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,970 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,972 INFO  L256         TraceCheckSpWp]: Trace formula consists of 436 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:38,975 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,015 INFO  L134       CoverageAnalysis]: Checked inductivity of 91 backedges. 55 proven. 6 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:39,015 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:39,361 INFO  L134       CoverageAnalysis]: Checked inductivity of 91 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 71 trivial. 0 not checked.
[2025-04-28 21:21:39,362 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [936908] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:39,362 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:39,362 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 6, 6] total 9
[2025-04-28 21:21:39,362 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2077484036]
[2025-04-28 21:21:39,362 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,363 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:39,363 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,363 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:39,363 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:39,365 INFO  L87              Difference]: Start difference. First operand 92 states and 364 transitions. Second operand  has 9 states, 4 states have (on average 4.5) internal successors, (18), 8 states have internal predecessors, (18), 8 states have call successors, (22), 2 states have call predecessors, (22), 4 states have return successors, (22), 4 states have call predecessors, (22), 8 states have call successors, (22)
[2025-04-28 21:21:39,964 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,965 INFO  L93              Difference]: Finished difference Result 101 states and 470 transitions.
[2025-04-28 21:21:39,965 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:39,965 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 4 states have (on average 4.5) internal successors, (18), 8 states have internal predecessors, (18), 8 states have call successors, (22), 2 states have call predecessors, (22), 4 states have return successors, (22), 4 states have call predecessors, (22), 8 states have call successors, (22) Word has length 48
[2025-04-28 21:21:39,965 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,970 INFO  L225             Difference]: With dead ends: 101
[2025-04-28 21:21:39,971 INFO  L226             Difference]: Without dead ends: 101
[2025-04-28 21:21:39,971 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 103 GetRequests, 95 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:39,972 INFO  L437           NwaCegarLoop]: 96 mSDtfsCounter, 4 mSDsluCounter, 315 mSDsCounter, 0 mSdLazyCounter, 479 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 411 SdHoareTripleChecker+Invalid, 487 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 479 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,972 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 411 Invalid, 487 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 479 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:39,973 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-04-28 21:21:40,045 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 99.
[2025-04-28 21:21:40,046 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 99 states, 17 states have (on average 1.7647058823529411) internal successors, (30), 29 states have internal predecessors, (30), 69 states have call successors, (69), 5 states have call predecessors, (69), 12 states have return successors, (369), 64 states have call predecessors, (369), 69 states have call successors, (369)
[2025-04-28 21:21:40,051 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 99 states to 99 states and 468 transitions.
[2025-04-28 21:21:40,051 INFO  L79                 Accepts]: Start accepts. Automaton has 99 states and 468 transitions. Word has length 48
[2025-04-28 21:21:40,053 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,053 INFO  L485      AbstractCegarLoop]: Abstraction has 99 states and 468 transitions.
[2025-04-28 21:21:40,053 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 4 states have (on average 4.5) internal successors, (18), 8 states have internal predecessors, (18), 8 states have call successors, (22), 2 states have call predecessors, (22), 4 states have return successors, (22), 4 states have call predecessors, (22), 8 states have call successors, (22)
[2025-04-28 21:21:40,053 INFO  L278                IsEmpty]: Start isEmpty. Operand 99 states and 468 transitions.
[2025-04-28 21:21:40,068 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 93
[2025-04-28 21:21:40,069 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,069 INFO  L218           NwaCegarLoop]: trace histogram [16, 16, 5, 4, 4, 4, 4, 4, 4, 4, 4, 4, 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,075 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:40,269 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,269 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,270 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,270 INFO  L85        PathProgramCache]: Analyzing trace with hash 1109320420, now seen corresponding path program 1 times
[2025-04-28 21:21:40,270 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,270 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2078419073]
[2025-04-28 21:21:40,270 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,270 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,288 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-04-28 21:21:40,333 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-04-28 21:21:40,333 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,333 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,182 INFO  L134       CoverageAnalysis]: Checked inductivity of 414 backedges. 14 proven. 82 refuted. 0 times theorem prover too weak. 318 trivial. 0 not checked.
[2025-04-28 21:21:41,182 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,182 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2078419073]
[2025-04-28 21:21:41,182 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2078419073] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,182 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1907731105]
[2025-04-28 21:21:41,182 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,183 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,185 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,187 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:41,191 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,299 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-04-28 21:21:41,435 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-04-28 21:21:41,435 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,436 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,441 INFO  L256         TraceCheckSpWp]: Trace formula consists of 922 conjuncts, 54 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,449 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,618 INFO  L134       CoverageAnalysis]: Checked inductivity of 414 backedges. 236 proven. 22 refuted. 0 times theorem prover too weak. 156 trivial. 0 not checked.
[2025-04-28 21:21:41,618 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:42,839 INFO  L134       CoverageAnalysis]: Checked inductivity of 414 backedges. 18 proven. 78 refuted. 0 times theorem prover too weak. 318 trivial. 0 not checked.
[2025-04-28 21:21:42,840 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1907731105] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:42,840 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:42,840 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 10, 10] total 18
[2025-04-28 21:21:42,840 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [465303145]
[2025-04-28 21:21:42,840 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,841 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:42,841 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,841 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:42,841 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=264, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:42,842 INFO  L87              Difference]: Start difference. First operand 99 states and 468 transitions. Second operand  has 18 states, 7 states have (on average 3.857142857142857) internal successors, (27), 15 states have internal predecessors, (27), 16 states have call successors, (36), 2 states have call predecessors, (36), 7 states have return successors, (36), 10 states have call predecessors, (36), 16 states have call successors, (36)
[2025-04-28 21:21:45,374 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,374 INFO  L93              Difference]: Finished difference Result 110 states and 650 transitions.
[2025-04-28 21:21:45,374 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:45,374 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 7 states have (on average 3.857142857142857) internal successors, (27), 15 states have internal predecessors, (27), 16 states have call successors, (36), 2 states have call predecessors, (36), 7 states have return successors, (36), 10 states have call predecessors, (36), 16 states have call successors, (36) Word has length 92
[2025-04-28 21:21:45,375 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,383 INFO  L225             Difference]: With dead ends: 110
[2025-04-28 21:21:45,383 INFO  L226             Difference]: Without dead ends: 110
[2025-04-28 21:21:45,383 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 204 GetRequests, 181 SyntacticMatches, 0 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 33 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=93, Invalid=507, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:45,384 INFO  L437           NwaCegarLoop]: 83 mSDtfsCounter, 18 mSDsluCounter, 702 mSDsCounter, 0 mSdLazyCounter, 1890 mSolverCounterSat, 127 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 66 SdHoareTripleChecker+Valid, 785 SdHoareTripleChecker+Invalid, 2017 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 127 IncrementalHoareTripleChecker+Valid, 1890 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,384 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [66 Valid, 785 Invalid, 2017 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [127 Valid, 1890 Invalid, 0 Unknown, 0 Unchecked, 2.2s Time]
[2025-04-28 21:21:45,385 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-04-28 21:21:45,485 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 100.
[2025-04-28 21:21:45,486 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 100 states, 17 states have (on average 1.7647058823529411) internal successors, (30), 29 states have internal predecessors, (30), 70 states have call successors, (70), 5 states have call predecessors, (70), 12 states have return successors, (373), 65 states have call predecessors, (373), 70 states have call successors, (373)
[2025-04-28 21:21:45,490 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 100 states to 100 states and 473 transitions.
[2025-04-28 21:21:45,490 INFO  L79                 Accepts]: Start accepts. Automaton has 100 states and 473 transitions. Word has length 92
[2025-04-28 21:21:45,490 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,491 INFO  L485      AbstractCegarLoop]: Abstraction has 100 states and 473 transitions.
[2025-04-28 21:21:45,491 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 7 states have (on average 3.857142857142857) internal successors, (27), 15 states have internal predecessors, (27), 16 states have call successors, (36), 2 states have call predecessors, (36), 7 states have return successors, (36), 10 states have call predecessors, (36), 16 states have call successors, (36)
[2025-04-28 21:21:45,491 INFO  L278                IsEmpty]: Start isEmpty. Operand 100 states and 473 transitions.
[2025-04-28 21:21:45,496 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 93
[2025-04-28 21:21:45,497 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,497 INFO  L218           NwaCegarLoop]: trace histogram [17, 16, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 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,504 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:45,698 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,698 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,700 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,700 INFO  L85        PathProgramCache]: Analyzing trace with hash 2078321811, now seen corresponding path program 1 times
[2025-04-28 21:21:45,700 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,700 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [674442910]
[2025-04-28 21:21:45,700 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,700 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,714 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-04-28 21:21:45,818 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-04-28 21:21:45,818 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,818 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,990 INFO  L134       CoverageAnalysis]: Checked inductivity of 450 backedges. 76 proven. 46 refuted. 0 times theorem prover too weak. 328 trivial. 0 not checked.
[2025-04-28 21:21:46,990 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,990 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [674442910]
[2025-04-28 21:21:46,991 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [674442910] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,991 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1739616055]
[2025-04-28 21:21:46,991 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,991 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,994 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,996 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:47,000 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,128 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 92 statements into 1 equivalence classes.
[2025-04-28 21:21:47,274 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 92 of 92 statements.
[2025-04-28 21:21:47,274 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,274 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,285 INFO  L256         TraceCheckSpWp]: Trace formula consists of 908 conjuncts, 70 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,291 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,623 INFO  L134       CoverageAnalysis]: Checked inductivity of 450 backedges. 70 proven. 50 refuted. 0 times theorem prover too weak. 330 trivial. 0 not checked.
[2025-04-28 21:21:47,624 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:49,472 INFO  L134       CoverageAnalysis]: Checked inductivity of 450 backedges. 70 proven. 50 refuted. 0 times theorem prover too weak. 330 trivial. 0 not checked.
[2025-04-28 21:21:49,472 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1739616055] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:49,472 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:49,472 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 12, 12] total 23
[2025-04-28 21:21:49,473 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1271951558]
[2025-04-28 21:21:49,473 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,473 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:49,473 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,474 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:49,474 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=443, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:49,474 INFO  L87              Difference]: Start difference. First operand 100 states and 473 transitions. Second operand  has 23 states, 8 states have (on average 3.25) internal successors, (26), 19 states have internal predecessors, (26), 18 states have call successors, (35), 1 states have call predecessors, (35), 8 states have return successors, (35), 13 states have call predecessors, (35), 18 states have call successors, (35)
