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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:34,619 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:34,722 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_49089ce7-1aab-4247-bc32-b8e45217976d/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:34,727 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:34,731 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:34,775 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:34,776 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:34,776 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:34,778 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:34,778 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:34,778 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:34,779 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:34,779 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:34,779 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:34,779 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:34,780 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:34,780 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:34,781 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:34,781 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:34,782 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:34,782 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:34,782 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:34,782 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:34,782 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:34,782 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:34,783 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:34,783 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:35,148 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:35,158 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:35,161 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:35,164 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:35,165 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:35,166 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_49089ce7-1aab-4247-bc32-b8e45217976d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-173.smt2
[2025-04-28 21:21:35,168 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:35,176 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:35,377 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_49089ce7-1aab-4247-bc32-b8e45217976d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-173.smt2
[2025-04-28 21:21:35,380 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:35,383 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:35,387 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:35,387 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:35,387 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:35,392 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,415 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35 Unit
[2025-04-28 21:21:35,416 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:35,418 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:35,418 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:35,418 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:35,433 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,434 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,463 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,463 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,465 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,466 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,468 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,469 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,469 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,487 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:35,489 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:35,489 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:35,489 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:35,490 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,493 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:35,509 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,526 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:35,532 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:35,548 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:35,548 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:35,548 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:35,548 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure %main given in one single declaration
[2025-04-28 21:21:35,548 INFO  L130     BoogieDeclarations]: Found specification of procedure %main
[2025-04-28 21:21:35,548 INFO  L138     BoogieDeclarations]: Found implementation of procedure %main
[2025-04-28 21:21:35,549 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure %main.2 given in one single declaration
[2025-04-28 21:21:35,549 INFO  L130     BoogieDeclarations]: Found specification of procedure %main.2
[2025-04-28 21:21:35,549 INFO  L138     BoogieDeclarations]: Found implementation of procedure %main.2
[2025-04-28 21:21:35,549 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure %main.3 given in one single declaration
[2025-04-28 21:21:35,549 INFO  L130     BoogieDeclarations]: Found specification of procedure %main.3
[2025-04-28 21:21:35,549 INFO  L138     BoogieDeclarations]: Found implementation of procedure %main.3
[2025-04-28 21:21:35,549 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:35,549 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:35,549 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:35,608 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:35,611 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:35,713 INFO  L?                        ?]: Removed 2 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:35,713 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:35,725 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:35,726 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:35,726 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:35 BoogieIcfgContainer
[2025-04-28 21:21:35,726 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:35,729 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:35,729 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:35,733 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:35,734 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:35" (1/3) ...
[2025-04-28 21:21:35,734 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@473ba041 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:35, skipping insertion in model container
[2025-04-28 21:21:35,734 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (2/3) ...
[2025-04-28 21:21:35,735 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@473ba041 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:35, skipping insertion in model container
[2025-04-28 21:21:35,735 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:35" (3/3) ...
[2025-04-28 21:21:35,736 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:35,756 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:35,760 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 5 procedures, 21 locations, 28 edges, 5 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:35,812 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:35,826 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;@7b9f370c, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:35,826 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:35,831 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 21 states, 10 states have (on average 1.3) internal successors, (13), 12 states have internal predecessors, (13), 5 states have call successors, (5), 4 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:35,838 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:35,838 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,839 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,840 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,849 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,850 INFO  L85        PathProgramCache]: Analyzing trace with hash 644221549, now seen corresponding path program 1 times
[2025-04-28 21:21:35,860 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,861 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [283644559]
[2025-04-28 21:21:35,862 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,863 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,912 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:35,939 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:35,939 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,939 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,231 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:36,231 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,231 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [283644559]
[2025-04-28 21:21:36,232 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [283644559] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,232 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,236 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:36,239 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [201582166]
[2025-04-28 21:21:36,240 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,245 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:36,248 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,282 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:36,283 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:36,285 INFO  L87              Difference]: Start difference. First operand  has 21 states, 10 states have (on average 1.3) internal successors, (13), 12 states have internal predecessors, (13), 5 states have call successors, (5), 4 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 5 states have call successors, (5) Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:36,375 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,376 INFO  L93              Difference]: Finished difference Result 25 states and 28 transitions.
[2025-04-28 21:21:36,381 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:36,383 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:21:36,383 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,392 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:21:36,392 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:21:36,394 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:36,399 INFO  L437           NwaCegarLoop]: 19 mSDtfsCounter, 2 mSDsluCounter, 48 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 67 SdHoareTripleChecker+Invalid, 17 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,400 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 67 Invalid, 17 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,423 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:21:36,454 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 23.
[2025-04-28 21:21:36,456 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 23 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 13 states have internal predecessors, (13), 5 states have call successors, (5), 4 states have call predecessors, (5), 6 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:36,506 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 23 states to 23 states and 25 transitions.
[2025-04-28 21:21:36,508 INFO  L79                 Accepts]: Start accepts. Automaton has 23 states and 25 transitions. Word has length 17
[2025-04-28 21:21:36,509 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,509 INFO  L485      AbstractCegarLoop]: Abstraction has 23 states and 25 transitions.
[2025-04-28 21:21:36,510 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:36,511 INFO  L278                IsEmpty]: Start isEmpty. Operand 23 states and 25 transitions.
[2025-04-28 21:21:36,512 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:36,512 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,513 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,513 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:36,513 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,514 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,515 INFO  L85        PathProgramCache]: Analyzing trace with hash 251194539, now seen corresponding path program 1 times
[2025-04-28 21:21:36,515 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,519 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [221994191]
[2025-04-28 21:21:36,520 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,520 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,528 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:36,536 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:36,539 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,539 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,672 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:36,672 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,672 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [221994191]
[2025-04-28 21:21:36,672 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [221994191] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,672 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,672 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:36,672 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [367530920]
[2025-04-28 21:21:36,673 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,674 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:36,674 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,674 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:36,675 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:36,676 INFO  L87              Difference]: Start difference. First operand 23 states and 25 transitions. Second operand  has 6 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 2 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:36,741 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,742 INFO  L93              Difference]: Finished difference Result 27 states and 29 transitions.
[2025-04-28 21:21:36,743 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:36,743 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 2 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 2 states have call successors, (4) Word has length 17
[2025-04-28 21:21:36,744 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,744 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:36,745 INFO  L226             Difference]: Without dead ends: 21
[2025-04-28 21:21:36,745 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:36,746 INFO  L437           NwaCegarLoop]: 21 mSDtfsCounter, 1 mSDsluCounter, 75 mSDsCounter, 0 mSdLazyCounter, 17 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 96 SdHoareTripleChecker+Invalid, 18 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 17 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,748 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 96 Invalid, 18 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 17 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,749 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 21 states.
[2025-04-28 21:21:36,753 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 21 to 21.
[2025-04-28 21:21:36,754 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 21 states, 10 states have (on average 1.1) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 4 states have call predecessors, (5), 5 states have return successors, (6), 5 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:36,755 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 21 states to 21 states and 22 transitions.
[2025-04-28 21:21:36,755 INFO  L79                 Accepts]: Start accepts. Automaton has 21 states and 22 transitions. Word has length 17
[2025-04-28 21:21:36,756 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,756 INFO  L485      AbstractCegarLoop]: Abstraction has 21 states and 22 transitions.
[2025-04-28 21:21:36,756 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 2 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:36,756 INFO  L278                IsEmpty]: Start isEmpty. Operand 21 states and 22 transitions.
[2025-04-28 21:21:36,757 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:36,757 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,757 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]
[2025-04-28 21:21:36,757 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:36,757 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,758 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,758 INFO  L85        PathProgramCache]: Analyzing trace with hash -1666125873, now seen corresponding path program 1 times
[2025-04-28 21:21:36,758 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,758 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [501319103]
[2025-04-28 21:21:36,758 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,758 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,775 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:36,788 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:36,792 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,792 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,048 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:37,048 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,049 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [501319103]
[2025-04-28 21:21:37,049 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [501319103] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,049 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [713717060]
[2025-04-28 21:21:37,049 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,049 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,055 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,059 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:37,061 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,117 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:37,138 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:37,138 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,139 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,141 INFO  L256         TraceCheckSpWp]: Trace formula consists of 58 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,150 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,288 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:37,290 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,049 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:38,050 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [713717060] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,050 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,050 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 9
[2025-04-28 21:21:38,050 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [150324127]
[2025-04-28 21:21:38,054 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,054 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:38,055 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,055 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:38,056 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=54, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:38,056 INFO  L87              Difference]: Start difference. First operand 21 states and 22 transitions. Second operand  has 9 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:38,154 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,155 INFO  L93              Difference]: Finished difference Result 23 states and 24 transitions.
[2025-04-28 21:21:38,156 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:38,156 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 5 states have call successors, (6) Word has length 21
[2025-04-28 21:21:38,157 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,158 INFO  L225             Difference]: With dead ends: 23
[2025-04-28 21:21:38,158 INFO  L226             Difference]: Without dead ends: 23
[2025-04-28 21:21:38,159 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 50 GetRequests, 39 SyntacticMatches, 3 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:38,160 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 4 mSDsluCounter, 69 mSDsCounter, 0 mSdLazyCounter, 33 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 87 SdHoareTripleChecker+Invalid, 35 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 33 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,161 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 87 Invalid, 35 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 33 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:38,163 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 23 states.
[2025-04-28 21:21:38,168 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 23 to 23.
[2025-04-28 21:21:38,168 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 23 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 5 states have call successors, (5), 4 states have call predecessors, (5), 6 states have return successors, (7), 6 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:38,169 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 23 states to 23 states and 24 transitions.
[2025-04-28 21:21:38,170 INFO  L79                 Accepts]: Start accepts. Automaton has 23 states and 24 transitions. Word has length 21
[2025-04-28 21:21:38,170 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,170 INFO  L485      AbstractCegarLoop]: Abstraction has 23 states and 24 transitions.
[2025-04-28 21:21:38,171 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:38,171 INFO  L278                IsEmpty]: Start isEmpty. Operand 23 states and 24 transitions.
[2025-04-28 21:21:38,171 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:38,171 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,171 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,179 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:38,372 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:38,372 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,373 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,373 INFO  L85        PathProgramCache]: Analyzing trace with hash -1787445583, now seen corresponding path program 2 times
[2025-04-28 21:21:38,373 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,373 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1862008299]
[2025-04-28 21:21:38,373 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:38,374 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,381 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:38,400 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:38,404 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:38,404 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,643 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:38,643 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,643 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1862008299]
[2025-04-28 21:21:38,643 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1862008299] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:38,643 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2033917023]
[2025-04-28 21:21:38,644 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:38,644 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,647 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:38,649 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:38,653 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:38,700 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:38,717 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:38,717 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:38,717 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,719 INFO  L256         TraceCheckSpWp]: Trace formula consists of 73 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:38,721 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:38,819 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:38,820 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,111 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:40,112 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2033917023] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,112 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,112 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 13
[2025-04-28 21:21:40,112 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2107304759]
[2025-04-28 21:21:40,112 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,112 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:40,112 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,113 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:40,113 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=127, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:40,113 INFO  L87              Difference]: Start difference. First operand 23 states and 24 transitions. Second operand  has 13 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 8 states have call successors, (9)
[2025-04-28 21:21:40,255 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,255 INFO  L93              Difference]: Finished difference Result 25 states and 26 transitions.
[2025-04-28 21:21:40,255 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:40,256 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 8 states have call successors, (9) Word has length 25
[2025-04-28 21:21:40,256 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,256 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:21:40,257 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:21:40,257 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 62 GetRequests, 44 SyntacticMatches, 4 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 24 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=51, Invalid=189, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:40,258 INFO  L437           NwaCegarLoop]: 19 mSDtfsCounter, 9 mSDsluCounter, 129 mSDsCounter, 0 mSdLazyCounter, 63 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 148 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 63 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,258 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 148 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 63 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:40,259 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:21:40,262 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 25.
[2025-04-28 21:21:40,262 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 25 states, 12 states have (on average 1.0833333333333333) internal successors, (13), 13 states have internal predecessors, (13), 5 states have call successors, (5), 4 states have call predecessors, (5), 7 states have return successors, (8), 7 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:40,263 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 26 transitions.
[2025-04-28 21:21:40,263 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 26 transitions. Word has length 25
[2025-04-28 21:21:40,263 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,263 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 26 transitions.
[2025-04-28 21:21:40,263 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 8 states have call successors, (9)
[2025-04-28 21:21:40,263 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 26 transitions.
[2025-04-28 21:21:40,264 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:40,264 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,264 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,270 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:40,468 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:40,468 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,469 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,469 INFO  L85        PathProgramCache]: Analyzing trace with hash -2139941101, now seen corresponding path program 3 times
[2025-04-28 21:21:40,469 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,469 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1150293487]
[2025-04-28 21:21:40,469 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:40,469 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,476 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 29 statements into 4 equivalence classes.
[2025-04-28 21:21:40,485 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:40,485 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:40,485 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,772 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 15 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:40,772 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,772 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1150293487]
[2025-04-28 21:21:40,772 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1150293487] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,772 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [935544456]
[2025-04-28 21:21:40,773 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:40,773 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,777 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,780 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:40,783 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,842 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 29 statements into 4 equivalence classes.
[2025-04-28 21:21:40,862 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:40,862 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:40,862 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,864 INFO  L256         TraceCheckSpWp]: Trace formula consists of 88 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,867 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,007 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 15 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:41,007 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,115 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 15 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:43,115 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [935544456] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,115 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,115 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 18
[2025-04-28 21:21:43,115 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1223659955]
[2025-04-28 21:21:43,116 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,117 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:43,117 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,118 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:43,119 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=47, Invalid=259, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:43,119 INFO  L87              Difference]: Start difference. First operand 25 states and 26 transitions. Second operand  has 18 states, 7 states have (on average 3.0) internal successors, (21), 18 states have internal predecessors, (21), 12 states have call successors, (13), 1 states have call predecessors, (13), 6 states have return successors, (13), 5 states have call predecessors, (13), 12 states have call successors, (13)
[2025-04-28 21:21:43,299 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,301 INFO  L93              Difference]: Finished difference Result 27 states and 28 transitions.
[2025-04-28 21:21:43,301 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:43,302 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 7 states have (on average 3.0) internal successors, (21), 18 states have internal predecessors, (21), 12 states have call successors, (13), 1 states have call predecessors, (13), 6 states have return successors, (13), 5 states have call predecessors, (13), 12 states have call successors, (13) Word has length 29
[2025-04-28 21:21:43,302 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,303 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:43,304 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:43,305 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 73 GetRequests, 49 SyntacticMatches, 4 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 59 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=89, Invalid=373, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:43,305 INFO  L437           NwaCegarLoop]: 20 mSDtfsCounter, 11 mSDsluCounter, 160 mSDsCounter, 0 mSdLazyCounter, 84 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 180 SdHoareTripleChecker+Invalid, 96 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 84 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,306 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 180 Invalid, 96 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 84 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:43,307 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:43,312 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:43,314 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 5 states have call successors, (5), 4 states have call predecessors, (5), 8 states have return successors, (9), 8 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:43,315 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 28 transitions.
[2025-04-28 21:21:43,315 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 28 transitions. Word has length 29
[2025-04-28 21:21:43,315 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,316 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 28 transitions.
[2025-04-28 21:21:43,317 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 7 states have (on average 3.0) internal successors, (21), 18 states have internal predecessors, (21), 12 states have call successors, (13), 1 states have call predecessors, (13), 6 states have return successors, (13), 5 states have call predecessors, (13), 12 states have call successors, (13)
[2025-04-28 21:21:43,317 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 28 transitions.
[2025-04-28 21:21:43,318 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:43,318 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,318 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,326 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:43,519 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:43,519 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,520 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,520 INFO  L85        PathProgramCache]: Analyzing trace with hash 1455397109, now seen corresponding path program 4 times
[2025-04-28 21:21:43,520 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,520 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2137870134]
[2025-04-28 21:21:43,520 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:43,520 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,527 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 33 statements into 2 equivalence classes.
[2025-04-28 21:21:43,535 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:43,536 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:43,536 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,811 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 26 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:43,812 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,812 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2137870134]
[2025-04-28 21:21:43,812 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2137870134] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,812 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [732274842]
[2025-04-28 21:21:43,812 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:43,812 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,816 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,819 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:43,821 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,900 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 33 statements into 2 equivalence classes.
[2025-04-28 21:21:43,917 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:43,917 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:43,917 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,918 INFO  L256         TraceCheckSpWp]: Trace formula consists of 103 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,920 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,038 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 25 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:44,038 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,080 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 26 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:47,084 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [732274842] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,084 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,084 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 13, 14] total 21
[2025-04-28 21:21:47,084 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [596331183]
[2025-04-28 21:21:47,085 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,085 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:47,085 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,086 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:47,086 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=57, Invalid=363, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:47,086 INFO  L87              Difference]: Start difference. First operand 27 states and 28 transitions. Second operand  has 21 states, 8 states have (on average 3.0) internal successors, (24), 21 states have internal predecessors, (24), 14 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (16), 6 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:21:47,356 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,356 INFO  L93              Difference]: Finished difference Result 29 states and 30 transitions.
[2025-04-28 21:21:47,357 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:47,357 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 8 states have (on average 3.0) internal successors, (24), 21 states have internal predecessors, (24), 14 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (16), 6 states have call predecessors, (16), 14 states have call successors, (16) Word has length 33
[2025-04-28 21:21:47,357 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,358 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:47,358 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:21:47,358 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 84 GetRequests, 55 SyntacticMatches, 5 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 81 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=120, Invalid=530, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:47,359 INFO  L437           NwaCegarLoop]: 21 mSDtfsCounter, 33 mSDsluCounter, 219 mSDsCounter, 0 mSdLazyCounter, 116 mSolverCounterSat, 39 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 240 SdHoareTripleChecker+Invalid, 155 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 39 IncrementalHoareTripleChecker+Valid, 116 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,359 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 240 Invalid, 155 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [39 Valid, 116 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:47,360 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:21:47,363 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:21:47,363 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 14 states have (on average 1.0714285714285714) internal successors, (15), 15 states have internal predecessors, (15), 5 states have call successors, (5), 4 states have call predecessors, (5), 9 states have return successors, (10), 9 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:21:47,364 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 30 transitions.
[2025-04-28 21:21:47,364 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 30 transitions. Word has length 33
[2025-04-28 21:21:47,364 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,364 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 30 transitions.
[2025-04-28 21:21:47,364 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 8 states have (on average 3.0) internal successors, (24), 21 states have internal predecessors, (24), 14 states have call successors, (15), 1 states have call predecessors, (15), 7 states have return successors, (16), 6 states have call predecessors, (16), 14 states have call successors, (16)
[2025-04-28 21:21:47,364 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 30 transitions.
[2025-04-28 21:21:47,365 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:47,365 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,365 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,372 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:47,566 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:47,566 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,567 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,567 INFO  L85        PathProgramCache]: Analyzing trace with hash 1690952791, now seen corresponding path program 5 times
[2025-04-28 21:21:47,567 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,567 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2010632755]
[2025-04-28 21:21:47,567 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,567 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,574 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 37 statements into 6 equivalence classes.
[2025-04-28 21:21:47,584 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:47,584 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:47,584 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,912 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 40 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:47,912 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,912 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2010632755]
[2025-04-28 21:21:47,912 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2010632755] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,913 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1602387392]
[2025-04-28 21:21:47,913 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,913 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,915 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,917 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:47,922 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,028 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 37 statements into 6 equivalence classes.
[2025-04-28 21:21:48,048 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:48,048 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:48,048 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,049 INFO  L256         TraceCheckSpWp]: Trace formula consists of 118 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,051 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,176 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 37 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:48,176 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,826 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 40 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:52,827 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1602387392] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,827 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,827 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 14, 16] total 24
[2025-04-28 21:21:52,827 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1232711124]
[2025-04-28 21:21:52,827 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,828 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:52,828 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,829 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:52,829 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=67, Invalid=485, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:52,829 INFO  L87              Difference]: Start difference. First operand 29 states and 30 transitions. Second operand  has 24 states, 9 states have (on average 3.0) internal successors, (27), 24 states have internal predecessors, (27), 16 states have call successors, (17), 1 states have call predecessors, (17), 8 states have return successors, (19), 7 states have call predecessors, (19), 16 states have call successors, (19)
[2025-04-28 21:21:53,080 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,080 INFO  L93              Difference]: Finished difference Result 31 states and 32 transitions.
[2025-04-28 21:21:53,083 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:53,084 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 9 states have (on average 3.0) internal successors, (27), 24 states have internal predecessors, (27), 16 states have call successors, (17), 1 states have call predecessors, (17), 8 states have return successors, (19), 7 states have call predecessors, (19), 16 states have call successors, (19) Word has length 37
[2025-04-28 21:21:53,084 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,084 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:53,084 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:53,085 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 95 GetRequests, 61 SyntacticMatches, 6 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 106 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=155, Invalid=715, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:53,086 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 23 mSDsluCounter, 246 mSDsCounter, 0 mSdLazyCounter, 138 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 268 SdHoareTripleChecker+Invalid, 164 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 138 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,086 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 268 Invalid, 164 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 138 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:53,087 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:53,090 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 31.
[2025-04-28 21:21:53,090 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 15 states have (on average 1.0666666666666667) internal successors, (16), 16 states have internal predecessors, (16), 5 states have call successors, (5), 4 states have call predecessors, (5), 10 states have return successors, (11), 10 states have call predecessors, (11), 5 states have call successors, (11)
[2025-04-28 21:21:53,091 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 32 transitions.
[2025-04-28 21:21:53,091 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 32 transitions. Word has length 37
[2025-04-28 21:21:53,091 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,092 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 32 transitions.
[2025-04-28 21:21:53,092 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 9 states have (on average 3.0) internal successors, (27), 24 states have internal predecessors, (27), 16 states have call successors, (17), 1 states have call predecessors, (17), 8 states have return successors, (19), 7 states have call predecessors, (19), 16 states have call successors, (19)
[2025-04-28 21:21:53,092 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 32 transitions.
[2025-04-28 21:21:53,093 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:53,093 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,093 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,100 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:53,297 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:53,298 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,298 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,298 INFO  L85        PathProgramCache]: Analyzing trace with hash -1806132935, now seen corresponding path program 6 times
[2025-04-28 21:21:53,298 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,298 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2082601758]
[2025-04-28 21:21:53,298 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:53,298 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,306 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 41 statements into 7 equivalence classes.
[2025-04-28 21:21:53,322 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:53,322 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:53,323 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,727 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 2 proven. 55 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:21:53,727 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,727 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2082601758]
[2025-04-28 21:21:53,727 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2082601758] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,728 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1260875234]
[2025-04-28 21:21:53,728 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:53,728 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,730 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,732 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:53,737 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,893 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 41 statements into 7 equivalence classes.
[2025-04-28 21:21:53,926 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:53,926 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:53,926 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,928 INFO  L256         TraceCheckSpWp]: Trace formula consists of 133 conjuncts, 29 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,930 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,091 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 51 refuted. 0 times theorem prover too weak. 27 trivial. 0 not checked.
[2025-04-28 21:21:54,091 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,395 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 57 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:22:01,399 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1260875234] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,399 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,399 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 15, 18] total 27
[2025-04-28 21:22:01,399 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1774851112]
[2025-04-28 21:22:01,399 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,400 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:22:01,421 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,422 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:22:01,422 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=87, Invalid=615, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:01,422 INFO  L87              Difference]: Start difference. First operand 31 states and 32 transitions. Second operand  has 27 states, 10 states have (on average 3.0) internal successors, (30), 27 states have internal predecessors, (30), 18 states have call successors, (19), 1 states have call predecessors, (19), 9 states have return successors, (22), 8 states have call predecessors, (22), 18 states have call successors, (22)
[2025-04-28 21:22:01,665 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,665 INFO  L93              Difference]: Finished difference Result 33 states and 34 transitions.
[2025-04-28 21:22:01,665 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:01,666 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 10 states have (on average 3.0) internal successors, (30), 27 states have internal predecessors, (30), 18 states have call successors, (19), 1 states have call predecessors, (19), 9 states have return successors, (22), 8 states have call predecessors, (22), 18 states have call successors, (22) Word has length 41
[2025-04-28 21:22:01,666 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,667 INFO  L225             Difference]: With dead ends: 33
[2025-04-28 21:22:01,667 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:22:01,667 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 105 GetRequests, 67 SyntacticMatches, 7 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 222 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=183, Invalid=873, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:01,668 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 29 mSDsluCounter, 256 mSDsCounter, 0 mSdLazyCounter, 148 mSolverCounterSat, 24 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 38 SdHoareTripleChecker+Valid, 279 SdHoareTripleChecker+Invalid, 172 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 24 IncrementalHoareTripleChecker+Valid, 148 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,668 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [38 Valid, 279 Invalid, 172 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [24 Valid, 148 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:01,669 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:22:01,671 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 33.
[2025-04-28 21:22:01,672 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 16 states have (on average 1.0625) internal successors, (17), 17 states have internal predecessors, (17), 5 states have call successors, (5), 4 states have call predecessors, (5), 11 states have return successors, (12), 11 states have call predecessors, (12), 5 states have call successors, (12)
[2025-04-28 21:22:01,672 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 34 transitions.
[2025-04-28 21:22:01,673 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 34 transitions. Word has length 41
[2025-04-28 21:22:01,673 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,673 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 34 transitions.
[2025-04-28 21:22:01,673 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 10 states have (on average 3.0) internal successors, (30), 27 states have internal predecessors, (30), 18 states have call successors, (19), 1 states have call predecessors, (19), 9 states have return successors, (22), 8 states have call predecessors, (22), 18 states have call successors, (22)
[2025-04-28 21:22:01,673 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 34 transitions.
[2025-04-28 21:22:01,674 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:22:01,674 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,674 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,680 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:01,878 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,879 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,879 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,879 INFO  L85        PathProgramCache]: Analyzing trace with hash 915036059, now seen corresponding path program 7 times
[2025-04-28 21:22:01,879 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,879 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [772005047]
[2025-04-28 21:22:01,880 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:01,880 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,888 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:22:01,901 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:22:01,901 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,901 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,417 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 77 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:22:02,417 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,417 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [772005047]
[2025-04-28 21:22:02,418 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [772005047] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,418 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1199296157]
[2025-04-28 21:22:02,418 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:02,418 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,420 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:02,423 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:02,427 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,656 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:22:02,678 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:22:02,679 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,679 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,680 INFO  L256         TraceCheckSpWp]: Trace formula consists of 148 conjuncts, 33 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,683 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,840 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 67 refuted. 0 times theorem prover too weak. 38 trivial. 0 not checked.
[2025-04-28 21:22:02,840 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
