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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:23,744 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:23,837 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d0c54fa2-76df-487b-b4b6-0e9ddd671407/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:23,845 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:23,845 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:23,878 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:23,878 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:23,879 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:23,879 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:23,879 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:23,879 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:23,879 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:23,880 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:23,881 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:23,882 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:23,883 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:23,883 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:23,883 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:23,883 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:23,884 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:23,884 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:23,884 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:23,884 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:23,884 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:23,884 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:23,885 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:23,885 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:24,201 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:24,214 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:24,217 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:24,220 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:24,220 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:24,222 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d0c54fa2-76df-487b-b4b6-0e9ddd671407/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-154.smt2
[2025-04-28 21:21:24,223 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:24,227 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:24,677 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d0c54fa2-76df-487b-b4b6-0e9ddd671407/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-154.smt2
[2025-04-28 21:21:24,682 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:24,683 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:24,684 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:24,684 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:24,684 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:24,687 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,722 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24 Unit
[2025-04-28 21:21:24,725 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:24,726 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:24,726 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:24,727 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:24,747 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,748 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,782 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,782 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,790 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,792 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,799 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,800 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,801 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,828 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:24,829 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:24,829 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:24,829 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:24,830 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,833 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:24,851 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:24,867 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:24,872 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:24,890 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:24,891 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:24,891 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:24,891 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_42 given in one single declaration
[2025-04-28 21:21:24,891 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_42
[2025-04-28 21:21:24,891 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_42
[2025-04-28 21:21:24,891 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:24,891 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:24,891 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:24,942 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:24,944 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:25,409 INFO  L?                        ?]: Removed 1 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:25,410 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:25,421 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:25,422 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:25,422 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:25 BoogieIcfgContainer
[2025-04-28 21:21:25,423 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:25,425 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:25,425 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:25,430 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:25,430 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:24" (1/3) ...
[2025-04-28 21:21:25,431 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6d1ada8a and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:25, skipping insertion in model container
[2025-04-28 21:21:25,431 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (2/3) ...
[2025-04-28 21:21:25,431 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6d1ada8a and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:25, skipping insertion in model container
[2025-04-28 21:21:25,431 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:25" (3/3) ...
[2025-04-28 21:21:25,432 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:25,450 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:25,455 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 41 locations, 129 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:25,510 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:25,532 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;@4de861c6, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:25,532 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:25,539 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 41 states, 6 states have (on average 6.0) internal successors, (36), 36 states have internal predecessors, (36), 31 states have call successors, (31), 2 states have call predecessors, (31), 2 states have return successors, (31), 3 states have call predecessors, (31), 31 states have call successors, (31)
[2025-04-28 21:21:25,578 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:25,578 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,579 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:25,579 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,587 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,587 INFO  L85        PathProgramCache]: Analyzing trace with hash -1353516839, now seen corresponding path program 1 times
[2025-04-28 21:21:25,595 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,596 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1635920401]
[2025-04-28 21:21:25,596 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,597 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,628 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:25,649 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:25,650 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,650 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,791 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:25,792 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,792 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1635920401]
[2025-04-28 21:21:25,793 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1635920401] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:25,793 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:25,797 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:25,799 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [207030766]
[2025-04-28 21:21:25,799 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,804 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:25,805 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,839 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:25,839 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:25,841 INFO  L87              Difference]: Start difference. First operand  has 41 states, 6 states have (on average 6.0) internal successors, (36), 36 states have internal predecessors, (36), 31 states have call successors, (31), 2 states have call predecessors, (31), 2 states have return successors, (31), 3 states have call predecessors, (31), 31 states have call successors, (31) Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:26,260 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,261 INFO  L93              Difference]: Finished difference Result 41 states and 126 transitions.
[2025-04-28 21:21:26,266 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:26,268 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:26,268 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,282 INFO  L225             Difference]: With dead ends: 41
[2025-04-28 21:21:26,283 INFO  L226             Difference]: Without dead ends: 41
[2025-04-28 21:21:26,285 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:26,290 INFO  L437           NwaCegarLoop]: 67 mSDtfsCounter, 1 mSDsluCounter, 80 mSDsCounter, 0 mSdLazyCounter, 137 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 147 SdHoareTripleChecker+Invalid, 146 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 137 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,291 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 147 Invalid, 146 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 137 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:26,340 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 41 states.
[2025-04-28 21:21:26,400 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 41 to 41.
[2025-04-28 21:21:26,401 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 6 states have (on average 5.833333333333333) internal successors, (35), 35 states have internal predecessors, (35), 31 states have call successors, (31), 2 states have call predecessors, (31), 3 states have return successors, (60), 4 states have call predecessors, (60), 31 states have call successors, (60)
[2025-04-28 21:21:26,456 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 126 transitions.
[2025-04-28 21:21:26,458 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 126 transitions. Word has length 9
[2025-04-28 21:21:26,459 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,459 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 126 transitions.
[2025-04-28 21:21:26,459 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:26,459 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 126 transitions.
[2025-04-28 21:21:26,472 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:26,472 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,472 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,473 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:26,473 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,474 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,475 INFO  L85        PathProgramCache]: Analyzing trace with hash 189076786, now seen corresponding path program 1 times
[2025-04-28 21:21:26,475 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,475 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1842060058]
[2025-04-28 21:21:26,475 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,475 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,486 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:26,520 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:26,520 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,520 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,793 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:26,794 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,794 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1842060058]
[2025-04-28 21:21:26,794 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1842060058] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:26,794 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:26,794 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:26,794 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [199412781]
[2025-04-28 21:21:26,795 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,796 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:26,796 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,797 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:26,797 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:26,797 INFO  L87              Difference]: Start difference. First operand 41 states and 126 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:27,675 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,675 INFO  L93              Difference]: Finished difference Result 67 states and 404 transitions.
[2025-04-28 21:21:27,679 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:27,679 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 13
[2025-04-28 21:21:27,679 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,689 INFO  L225             Difference]: With dead ends: 67
[2025-04-28 21:21:27,689 INFO  L226             Difference]: Without dead ends: 67
[2025-04-28 21:21:27,690 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:27,691 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 15 mSDsluCounter, 14 mSDsCounter, 0 mSdLazyCounter, 312 mSolverCounterSat, 59 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 57 SdHoareTripleChecker+Valid, 101 SdHoareTripleChecker+Invalid, 371 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 59 IncrementalHoareTripleChecker+Valid, 312 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,691 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [57 Valid, 101 Invalid, 371 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [59 Valid, 312 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:27,692 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 67 states.
[2025-04-28 21:21:27,772 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 67 to 59.
[2025-04-28 21:21:27,773 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 59 states, 9 states have (on average 7.444444444444445) internal successors, (67), 50 states have internal predecessors, (67), 44 states have call successors, (44), 3 states have call predecessors, (44), 5 states have return successors, (145), 6 states have call predecessors, (145), 44 states have call successors, (145)
[2025-04-28 21:21:27,776 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 59 states to 59 states and 256 transitions.
[2025-04-28 21:21:27,776 INFO  L79                 Accepts]: Start accepts. Automaton has 59 states and 256 transitions. Word has length 13
[2025-04-28 21:21:27,776 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,776 INFO  L485      AbstractCegarLoop]: Abstraction has 59 states and 256 transitions.
[2025-04-28 21:21:27,777 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:27,777 INFO  L278                IsEmpty]: Start isEmpty. Operand 59 states and 256 transitions.
[2025-04-28 21:21:27,787 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:27,787 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,788 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,788 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:27,788 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,789 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,789 INFO  L85        PathProgramCache]: Analyzing trace with hash -56174067, now seen corresponding path program 1 times
[2025-04-28 21:21:27,789 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,789 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [425564926]
[2025-04-28 21:21:27,789 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,789 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,795 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:27,809 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:27,809 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,809 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,915 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:27,915 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,915 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [425564926]
[2025-04-28 21:21:27,915 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [425564926] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,915 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,915 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:27,915 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1329434282]
[2025-04-28 21:21:27,916 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,916 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:27,916 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,917 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:27,917 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:27,917 INFO  L87              Difference]: Start difference. First operand 59 states and 256 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:28,400 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,400 INFO  L93              Difference]: Finished difference Result 67 states and 391 transitions.
[2025-04-28 21:21:28,400 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:28,401 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 13
[2025-04-28 21:21:28,401 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,410 INFO  L225             Difference]: With dead ends: 67
[2025-04-28 21:21:28,410 INFO  L226             Difference]: Without dead ends: 67
[2025-04-28 21:21:28,411 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,412 INFO  L437           NwaCegarLoop]: 76 mSDtfsCounter, 1 mSDsluCounter, 25 mSDsCounter, 0 mSdLazyCounter, 260 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 101 SdHoareTripleChecker+Invalid, 272 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 260 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,412 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 101 Invalid, 272 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 260 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:28,413 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 67 states.
[2025-04-28 21:21:28,465 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 67 to 65.
[2025-04-28 21:21:28,468 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 65 states, 12 states have (on average 5.833333333333333) internal successors, (70), 53 states have internal predecessors, (70), 44 states have call successors, (44), 3 states have call predecessors, (44), 8 states have return successors, (242), 8 states have call predecessors, (242), 44 states have call successors, (242)
[2025-04-28 21:21:28,474 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 65 states to 65 states and 356 transitions.
[2025-04-28 21:21:28,474 INFO  L79                 Accepts]: Start accepts. Automaton has 65 states and 356 transitions. Word has length 13
[2025-04-28 21:21:28,474 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,475 INFO  L485      AbstractCegarLoop]: Abstraction has 65 states and 356 transitions.
[2025-04-28 21:21:28,475 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:28,475 INFO  L278                IsEmpty]: Start isEmpty. Operand 65 states and 356 transitions.
[2025-04-28 21:21:28,485 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:28,485 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,486 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,486 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:28,486 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,487 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,489 INFO  L85        PathProgramCache]: Analyzing trace with hash 264478120, now seen corresponding path program 1 times
[2025-04-28 21:21:28,489 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,489 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1896433742]
[2025-04-28 21:21:28,489 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,489 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,495 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:28,502 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:28,505 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,505 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,604 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:28,604 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,604 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1896433742]
[2025-04-28 21:21:28,604 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1896433742] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,604 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1078884691]
[2025-04-28 21:21:28,604 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,604 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,607 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,610 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:28,611 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,638 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:28,648 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:28,649 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,649 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,650 INFO  L256         TraceCheckSpWp]: Trace formula consists of 66 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,655 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,746 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:28,746 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:29,062 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:29,062 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1078884691] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:29,062 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:29,062 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:29,062 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [793024138]
[2025-04-28 21:21:29,062 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,062 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:29,063 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,063 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:29,063 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:29,063 INFO  L87              Difference]: Start difference. First operand 65 states and 356 transitions. Second operand  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:29,954 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,955 INFO  L93              Difference]: Finished difference Result 81 states and 635 transitions.
[2025-04-28 21:21:29,956 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:29,957 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7) Word has length 13
[2025-04-28 21:21:29,957 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,966 INFO  L225             Difference]: With dead ends: 81
[2025-04-28 21:21:29,966 INFO  L226             Difference]: Without dead ends: 81
[2025-04-28 21:21:29,967 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=31, Invalid=79, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:29,967 INFO  L437           NwaCegarLoop]: 75 mSDtfsCounter, 5 mSDsluCounter, 197 mSDsCounter, 0 mSdLazyCounter, 633 mSolverCounterSat, 51 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 272 SdHoareTripleChecker+Invalid, 684 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 51 IncrementalHoareTripleChecker+Valid, 633 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,968 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 272 Invalid, 684 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [51 Valid, 633 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:29,970 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 81 states.
[2025-04-28 21:21:30,041 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 81 to 71.
[2025-04-28 21:21:30,042 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 71 states, 15 states have (on average 4.866666666666666) internal successors, (73), 56 states have internal predecessors, (73), 44 states have call successors, (44), 3 states have call predecessors, (44), 11 states have return successors, (336), 11 states have call predecessors, (336), 44 states have call successors, (336)
[2025-04-28 21:21:30,045 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 71 states to 71 states and 453 transitions.
[2025-04-28 21:21:30,045 INFO  L79                 Accepts]: Start accepts. Automaton has 71 states and 453 transitions. Word has length 13
[2025-04-28 21:21:30,046 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,046 INFO  L485      AbstractCegarLoop]: Abstraction has 71 states and 453 transitions.
[2025-04-28 21:21:30,046 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:30,046 INFO  L278                IsEmpty]: Start isEmpty. Operand 71 states and 453 transitions.
[2025-04-28 21:21:30,055 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:30,055 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,055 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,060 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:30,255 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,256 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,256 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,256 INFO  L85        PathProgramCache]: Analyzing trace with hash -1898632833, now seen corresponding path program 1 times
[2025-04-28 21:21:30,256 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,256 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2058077428]
[2025-04-28 21:21:30,256 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,257 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,261 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:30,265 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:30,268 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,268 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,399 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:30,399 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,399 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2058077428]
[2025-04-28 21:21:30,399 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2058077428] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,399 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [781102274]
[2025-04-28 21:21:30,399 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,400 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,402 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,404 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:30,408 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:30,432 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:30,443 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:30,443 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,443 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,444 INFO  L256         TraceCheckSpWp]: Trace formula consists of 69 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:30,445 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,488 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:30,488 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:30,899 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:30,899 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [781102274] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,899 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:30,899 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6, 6] total 9
[2025-04-28 21:21:30,900 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [33005452]
[2025-04-28 21:21:30,900 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,900 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:30,900 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,901 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:30,901 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=52, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:30,902 INFO  L87              Difference]: Start difference. First operand 71 states and 453 transitions. Second operand  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:31,790 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,790 INFO  L93              Difference]: Finished difference Result 88 states and 644 transitions.
[2025-04-28 21:21:31,791 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:31,791 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-04-28 21:21:31,791 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,799 INFO  L225             Difference]: With dead ends: 88
[2025-04-28 21:21:31,799 INFO  L226             Difference]: Without dead ends: 88
[2025-04-28 21:21:31,799 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 31 GetRequests, 23 SyntacticMatches, 1 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=20, Invalid=52, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:31,801 INFO  L437           NwaCegarLoop]: 83 mSDtfsCounter, 16 mSDsluCounter, 63 mSDsCounter, 0 mSdLazyCounter, 543 mSolverCounterSat, 38 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 74 SdHoareTripleChecker+Valid, 146 SdHoareTripleChecker+Invalid, 581 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 38 IncrementalHoareTripleChecker+Valid, 543 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,801 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [74 Valid, 146 Invalid, 581 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [38 Valid, 543 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:31,802 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 88 states.
[2025-04-28 21:21:31,868 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 88 to 78.
[2025-04-28 21:21:31,870 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 18 states have (on average 4.055555555555555) internal successors, (73), 61 states have internal predecessors, (73), 45 states have call successors, (45), 3 states have call predecessors, (45), 14 states have return successors, (378), 13 states have call predecessors, (378), 45 states have call successors, (378)
[2025-04-28 21:21:31,873 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 496 transitions.
[2025-04-28 21:21:31,874 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 496 transitions. Word has length 13
[2025-04-28 21:21:31,874 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,874 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 496 transitions.
[2025-04-28 21:21:31,874 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:31,874 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 496 transitions.
[2025-04-28 21:21:31,883 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:31,883 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,883 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,888 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:32,084 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,084 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,085 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,085 INFO  L85        PathProgramCache]: Analyzing trace with hash -791926626, now seen corresponding path program 1 times
[2025-04-28 21:21:32,085 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,085 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [452795904]
[2025-04-28 21:21:32,085 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,085 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,089 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:32,093 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:32,094 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,094 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,161 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:32,162 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,162 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [452795904]
[2025-04-28 21:21:32,162 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [452795904] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,162 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:32,162 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:32,162 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1273599519]
[2025-04-28 21:21:32,162 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,163 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:32,163 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,163 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:32,163 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:32,163 INFO  L87              Difference]: Start difference. First operand 78 states and 496 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:32,743 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,744 INFO  L93              Difference]: Finished difference Result 94 states and 672 transitions.
[2025-04-28 21:21:32,745 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:32,745 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 13
[2025-04-28 21:21:32,745 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,753 INFO  L225             Difference]: With dead ends: 94
[2025-04-28 21:21:32,754 INFO  L226             Difference]: Without dead ends: 94
[2025-04-28 21:21:32,754 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:32,756 INFO  L437           NwaCegarLoop]: 89 mSDtfsCounter, 12 mSDsluCounter, 14 mSDsCounter, 0 mSdLazyCounter, 281 mSolverCounterSat, 61 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 48 SdHoareTripleChecker+Valid, 103 SdHoareTripleChecker+Invalid, 342 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 61 IncrementalHoareTripleChecker+Valid, 281 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,756 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [48 Valid, 103 Invalid, 342 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [61 Valid, 281 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:32,757 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-04-28 21:21:32,822 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 78.
[2025-04-28 21:21:32,823 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 18 states have (on average 4.055555555555555) internal successors, (73), 61 states have internal predecessors, (73), 45 states have call successors, (45), 3 states have call predecessors, (45), 14 states have return successors, (338), 14 states have call predecessors, (338), 45 states have call successors, (338)
[2025-04-28 21:21:32,827 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 456 transitions.
[2025-04-28 21:21:32,828 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 456 transitions. Word has length 13
[2025-04-28 21:21:32,828 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,829 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 456 transitions.
[2025-04-28 21:21:32,829 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:32,829 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 456 transitions.
[2025-04-28 21:21:32,837 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:32,838 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,838 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,838 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:32,838 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,838 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,839 INFO  L85        PathProgramCache]: Analyzing trace with hash -78247429, now seen corresponding path program 1 times
[2025-04-28 21:21:32,839 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,839 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [282780697]
[2025-04-28 21:21:32,839 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,839 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,842 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:32,849 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:32,849 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,849 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,981 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:32,981 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,981 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [282780697]
[2025-04-28 21:21:32,981 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [282780697] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:32,981 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [589886543]
[2025-04-28 21:21:32,981 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,981 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,984 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:32,986 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:32,989 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,023 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:33,033 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:33,033 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,033 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,034 INFO  L256         TraceCheckSpWp]: Trace formula consists of 71 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,036 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,098 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:33,098 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,362 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:33,363 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [589886543] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,363 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,363 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:33,363 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1154378270]
[2025-04-28 21:21:33,363 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,363 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:33,364 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,364 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:33,364 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=66, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:33,364 INFO  L87              Difference]: Start difference. First operand 78 states and 456 transitions. Second operand  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:34,302 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,302 INFO  L93              Difference]: Finished difference Result 124 states and 1067 transitions.
[2025-04-28 21:21:34,302 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:34,303 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 13
[2025-04-28 21:21:34,303 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,314 INFO  L225             Difference]: With dead ends: 124
[2025-04-28 21:21:34,314 INFO  L226             Difference]: Without dead ends: 124
[2025-04-28 21:21:34,314 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 34 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=46, Invalid=110, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:34,315 INFO  L437           NwaCegarLoop]: 71 mSDtfsCounter, 7 mSDsluCounter, 86 mSDsCounter, 0 mSdLazyCounter, 640 mSolverCounterSat, 55 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 60 SdHoareTripleChecker+Valid, 157 SdHoareTripleChecker+Invalid, 695 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 55 IncrementalHoareTripleChecker+Valid, 640 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,316 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [60 Valid, 157 Invalid, 695 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [55 Valid, 640 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:34,317 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 124 states.
[2025-04-28 21:21:34,426 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 124 to 84.
[2025-04-28 21:21:34,427 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 21 states have (on average 3.619047619047619) internal successors, (76), 64 states have internal predecessors, (76), 45 states have call successors, (45), 3 states have call predecessors, (45), 17 states have return successors, (399), 16 states have call predecessors, (399), 45 states have call successors, (399)
[2025-04-28 21:21:34,430 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 520 transitions.
[2025-04-28 21:21:34,430 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 520 transitions. Word has length 13
[2025-04-28 21:21:34,430 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,430 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 520 transitions.
[2025-04-28 21:21:34,431 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:34,431 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 520 transitions.
[2025-04-28 21:21:34,440 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:34,440 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,441 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,445 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:34,641 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,642 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,642 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,643 INFO  L85        PathProgramCache]: Analyzing trace with hash -1527679185, now seen corresponding path program 1 times
[2025-04-28 21:21:34,643 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,643 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1340406936]
[2025-04-28 21:21:34,643 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,643 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,647 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:34,654 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:34,658 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,658 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,764 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:34,764 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,764 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1340406936]
[2025-04-28 21:21:34,764 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1340406936] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,764 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1052605142]
[2025-04-28 21:21:34,765 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,765 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,767 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,769 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:34,772 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,803 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:34,813 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:34,813 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,813 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,815 INFO  L256         TraceCheckSpWp]: Trace formula consists of 69 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,816 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,879 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:34,879 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:35,118 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:35,118 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1052605142] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:35,118 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:35,121 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:35,121 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [709787893]
[2025-04-28 21:21:35,121 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,121 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:35,121 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,122 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:35,122 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=66, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:35,122 INFO  L87              Difference]: Start difference. First operand 84 states and 520 transitions. Second operand  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:35,850 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,850 INFO  L93              Difference]: Finished difference Result 110 states and 840 transitions.
[2025-04-28 21:21:35,850 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:35,850 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 13
[2025-04-28 21:21:35,851 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,868 INFO  L225             Difference]: With dead ends: 110
[2025-04-28 21:21:35,868 INFO  L226             Difference]: Without dead ends: 110
[2025-04-28 21:21:35,869 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=38, Invalid=94, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:35,870 INFO  L437           NwaCegarLoop]: 81 mSDtfsCounter, 6 mSDsluCounter, 211 mSDsCounter, 0 mSdLazyCounter, 585 mSolverCounterSat, 30 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 292 SdHoareTripleChecker+Invalid, 615 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 30 IncrementalHoareTripleChecker+Valid, 585 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,870 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 292 Invalid, 615 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [30 Valid, 585 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:35,871 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-04-28 21:21:35,937 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 84.
[2025-04-28 21:21:35,942 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 21 states have (on average 3.619047619047619) internal successors, (76), 64 states have internal predecessors, (76), 45 states have call successors, (45), 3 states have call predecessors, (45), 17 states have return successors, (399), 16 states have call predecessors, (399), 45 states have call successors, (399)
[2025-04-28 21:21:35,945 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 520 transitions.
[2025-04-28 21:21:35,945 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 520 transitions. Word has length 13
[2025-04-28 21:21:35,945 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,945 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 520 transitions.
[2025-04-28 21:21:35,945 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:35,945 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 520 transitions.
[2025-04-28 21:21:35,955 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:35,955 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,956 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,960 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:36,159 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,160 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,161 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,161 INFO  L85        PathProgramCache]: Analyzing trace with hash 2031535552, now seen corresponding path program 1 times
[2025-04-28 21:21:36,161 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,161 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [579301871]
[2025-04-28 21:21:36,161 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,161 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,165 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:36,169 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:36,169 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,169 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,244 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:36,245 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,245 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [579301871]
[2025-04-28 21:21:36,245 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [579301871] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,245 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,245 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:36,245 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1181464236]
[2025-04-28 21:21:36,245 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,245 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:36,245 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,246 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:36,246 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:36,246 INFO  L87              Difference]: Start difference. First operand 84 states and 520 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:36,679 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,681 INFO  L93              Difference]: Finished difference Result 94 states and 629 transitions.
[2025-04-28 21:21:36,681 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:36,682 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 13
[2025-04-28 21:21:36,682 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,687 INFO  L225             Difference]: With dead ends: 94
[2025-04-28 21:21:36,687 INFO  L226             Difference]: Without dead ends: 94
[2025-04-28 21:21:36,687 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:36,688 INFO  L437           NwaCegarLoop]: 95 mSDtfsCounter, 11 mSDsluCounter, 29 mSDsCounter, 0 mSdLazyCounter, 274 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 45 SdHoareTripleChecker+Valid, 124 SdHoareTripleChecker+Invalid, 302 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 274 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,688 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [45 Valid, 124 Invalid, 302 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 274 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:36,689 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-04-28 21:21:36,746 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 84.
[2025-04-28 21:21:36,746 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 21 states have (on average 3.619047619047619) internal successors, (76), 64 states have internal predecessors, (76), 45 states have call successors, (45), 3 states have call predecessors, (45), 17 states have return successors, (389), 16 states have call predecessors, (389), 45 states have call successors, (389)
[2025-04-28 21:21:36,749 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 510 transitions.
[2025-04-28 21:21:36,749 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 510 transitions. Word has length 13
[2025-04-28 21:21:36,750 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,750 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 510 transitions.
[2025-04-28 21:21:36,750 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:36,750 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 510 transitions.
[2025-04-28 21:21:36,757 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[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 [3, 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: SelfDestructingSolverStorable9
[2025-04-28 21:21:36,758 INFO  L403      AbstractCegarLoop]: === Iteration 10 === 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 -1457255427, 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 [1342801211]
[2025-04-28 21:21:36,758 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,759 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,762 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:36,767 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,767 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,767 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,841 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:36,841 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,841 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1342801211]
[2025-04-28 21:21:36,841 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1342801211] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,841 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1434537720]
[2025-04-28 21:21:36,841 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,841 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,844 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,846 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:36,850 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,881 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:36,895 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,895 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,895 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,896 INFO  L256         TraceCheckSpWp]: Trace formula consists of 101 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,897 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,951 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:36,952 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:36,952 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1434537720] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,952 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:36,952 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [6] total 8
[2025-04-28 21:21:36,952 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1664725379]
[2025-04-28 21:21:36,952 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,952 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:36,953 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,953 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:36,953 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:36,953 INFO  L87              Difference]: Start difference. First operand 84 states and 510 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:37,328 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,328 INFO  L93              Difference]: Finished difference Result 117 states and 768 transitions.
[2025-04-28 21:21:37,328 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:37,329 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:37,329 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,334 INFO  L225             Difference]: With dead ends: 117
[2025-04-28 21:21:37,335 INFO  L226             Difference]: Without dead ends: 117
[2025-04-28 21:21:37,335 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 24 GetRequests, 17 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=18, Invalid=54, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:37,335 INFO  L437           NwaCegarLoop]: 121 mSDtfsCounter, 9 mSDsluCounter, 64 mSDsCounter, 0 mSdLazyCounter, 195 mSolverCounterSat, 69 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 185 SdHoareTripleChecker+Invalid, 264 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 69 IncrementalHoareTripleChecker+Valid, 195 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,336 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 185 Invalid, 264 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [69 Valid, 195 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:37,336 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 117 states.
[2025-04-28 21:21:37,386 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 117 to 95.
[2025-04-28 21:21:37,387 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 95 states, 24 states have (on average 4.5) internal successors, (108), 73 states have internal predecessors, (108), 51 states have call successors, (51), 4 states have call predecessors, (51), 19 states have return successors, (357), 18 states have call predecessors, (357), 51 states have call successors, (357)
[2025-04-28 21:21:37,390 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 95 states to 95 states and 516 transitions.
[2025-04-28 21:21:37,390 INFO  L79                 Accepts]: Start accepts. Automaton has 95 states and 516 transitions. Word has length 17
[2025-04-28 21:21:37,390 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,390 INFO  L485      AbstractCegarLoop]: Abstraction has 95 states and 516 transitions.
[2025-04-28 21:21:37,390 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:37,390 INFO  L278                IsEmpty]: Start isEmpty. Operand 95 states and 516 transitions.
[2025-04-28 21:21:37,398 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:37,398 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,398 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,403 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:37,602 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,602 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,602 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,602 INFO  L85        PathProgramCache]: Analyzing trace with hash -275247848, now seen corresponding path program 1 times
[2025-04-28 21:21:37,603 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,603 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1708296945]
[2025-04-28 21:21:37,603 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,603 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,607 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:37,617 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:37,618 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,618 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,706 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:37,706 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,706 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1708296945]
[2025-04-28 21:21:37,706 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1708296945] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,706 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [700742615]
[2025-04-28 21:21:37,707 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,707 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,710 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,712 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:37,716 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,751 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:37,765 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:37,765 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,765 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,766 INFO  L256         TraceCheckSpWp]: Trace formula consists of 95 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,769 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,800 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:37,800 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,351 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:38,352 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [700742615] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:38,352 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:38,352 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6, 6] total 9
[2025-04-28 21:21:38,353 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [40798660]
[2025-04-28 21:21:38,353 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,354 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:38,354 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,354 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:38,354 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=52, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:38,354 INFO  L87              Difference]: Start difference. First operand 95 states and 516 transitions. Second operand  has 6 states, 4 states have (on average 2.0) internal successors, (8), 6 states have internal predecessors, (8), 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:38,822 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,822 INFO  L93              Difference]: Finished difference Result 123 states and 819 transitions.
[2025-04-28 21:21:38,823 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:38,823 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 6 states have internal predecessors, (8), 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:38,824 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,830 INFO  L225             Difference]: With dead ends: 123
[2025-04-28 21:21:38,830 INFO  L226             Difference]: Without dead ends: 123
[2025-04-28 21:21:38,830 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 40 GetRequests, 31 SyntacticMatches, 2 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=20, Invalid=52, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:38,830 INFO  L437           NwaCegarLoop]: 77 mSDtfsCounter, 2 mSDsluCounter, 94 mSDsCounter, 0 mSdLazyCounter, 377 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 171 SdHoareTripleChecker+Invalid, 393 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 377 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,831 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 171 Invalid, 393 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 377 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:38,832 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 123 states.
[2025-04-28 21:21:38,902 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 123 to 107.
[2025-04-28 21:21:38,903 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 107 states, 30 states have (on average 3.8) internal successors, (114), 79 states have internal predecessors, (114), 51 states have call successors, (51), 4 states have call predecessors, (51), 25 states have return successors, (463), 24 states have call predecessors, (463), 51 states have call successors, (463)
[2025-04-28 21:21:38,906 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 107 states to 107 states and 628 transitions.
[2025-04-28 21:21:38,906 INFO  L79                 Accepts]: Start accepts. Automaton has 107 states and 628 transitions. Word has length 17
[2025-04-28 21:21:38,906 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,906 INFO  L485      AbstractCegarLoop]: Abstraction has 107 states and 628 transitions.
[2025-04-28 21:21:38,907 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.0) internal successors, (8), 6 states have internal predecessors, (8), 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:38,907 INFO  L278                IsEmpty]: Start isEmpty. Operand 107 states and 628 transitions.
[2025-04-28 21:21:38,915 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:38,915 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,915 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,921 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:39,119 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,119 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,120 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,120 INFO  L85        PathProgramCache]: Analyzing trace with hash 648399469, now seen corresponding path program 1 times
[2025-04-28 21:21:39,120 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,120 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2126604553]
[2025-04-28 21:21:39,121 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,121 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,124 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:39,129 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:39,129 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,129 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,224 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:39,224 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,224 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2126604553]
[2025-04-28 21:21:39,224 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2126604553] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,226 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1182629003]
[2025-04-28 21:21:39,226 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,226 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,228 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,231 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:39,235 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,277 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:39,290 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:39,291 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,291 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,292 INFO  L256         TraceCheckSpWp]: Trace formula consists of 97 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,293 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,341 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:39,342 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:39,535 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:39,535 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1182629003] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:39,535 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:39,535 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:39,535 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [512704219]
[2025-04-28 21:21:39,535 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,535 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:39,536 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,536 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:39,536 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:39,536 INFO  L87              Difference]: Start difference. First operand 107 states and 628 transitions. Second operand  has 10 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 5 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:42,238 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,239 INFO  L93              Difference]: Finished difference Result 252 states and 1291 transitions.
[2025-04-28 21:21:42,239 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 37 states. 
[2025-04-28 21:21:42,239 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 5 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7) Word has length 17
[2025-04-28 21:21:42,239 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,251 INFO  L225             Difference]: With dead ends: 252
[2025-04-28 21:21:42,251 INFO  L226             Difference]: Without dead ends: 246
[2025-04-28 21:21:42,252 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 69 GetRequests, 28 SyntacticMatches, 4 SemanticMatches, 37 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 368 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=295, Invalid=1187, Unknown=0, NotChecked=0, Total=1482
[2025-04-28 21:21:42,253 INFO  L437           NwaCegarLoop]: 98 mSDtfsCounter, 53 mSDsluCounter, 71 mSDsCounter, 0 mSdLazyCounter, 1724 mSolverCounterSat, 693 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 85 SdHoareTripleChecker+Valid, 169 SdHoareTripleChecker+Invalid, 2417 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 693 IncrementalHoareTripleChecker+Valid, 1724 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,253 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [85 Valid, 169 Invalid, 2417 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [693 Valid, 1724 Invalid, 0 Unknown, 0 Unchecked, 2.3s Time]
[2025-04-28 21:21:42,255 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 246 states.
[2025-04-28 21:21:42,330 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 246 to 162.
[2025-04-28 21:21:42,331 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 162 states, 51 states have (on average 4.313725490196078) internal successors, (220), 114 states have internal predecessors, (220), 69 states have call successors, (69), 9 states have call predecessors, (69), 41 states have return successors, (526), 39 states have call predecessors, (526), 69 states have call successors, (526)
[2025-04-28 21:21:42,335 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 162 states to 162 states and 815 transitions.
[2025-04-28 21:21:42,336 INFO  L79                 Accepts]: Start accepts. Automaton has 162 states and 815 transitions. Word has length 17
[2025-04-28 21:21:42,336 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,336 INFO  L485      AbstractCegarLoop]: Abstraction has 162 states and 815 transitions.
[2025-04-28 21:21:42,336 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 10 states have internal predecessors, (14), 5 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:42,336 INFO  L278                IsEmpty]: Start isEmpty. Operand 162 states and 815 transitions.
[2025-04-28 21:21:42,345 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:42,345 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,345 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,349 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:42,549 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:42,549 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,549 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,549 INFO  L85        PathProgramCache]: Analyzing trace with hash -324087143, now seen corresponding path program 1 times
[2025-04-28 21:21:42,549 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,549 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [432379194]
[2025-04-28 21:21:42,549 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,550 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,552 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:42,557 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:42,558 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,558 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,676 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:42,676 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,676 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [432379194]
[2025-04-28 21:21:42,682 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [432379194] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,682 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [466215379]
[2025-04-28 21:21:42,682 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,682 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,685 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,687 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:42,696 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,731 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:42,743 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:42,743 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,744 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,744 INFO  L256         TraceCheckSpWp]: Trace formula consists of 94 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,745 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,794 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:42,794 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:42,794 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [466215379] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,794 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:42,794 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [6] total 6
[2025-04-28 21:21:42,794 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [958141644]
[2025-04-28 21:21:42,795 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,795 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:42,795 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,795 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:42,795 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,796 INFO  L87              Difference]: Start difference. First operand 162 states and 815 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:43,113 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,113 INFO  L93              Difference]: Finished difference Result 180 states and 701 transitions.
[2025-04-28 21:21:43,114 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:43,114 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:43,114 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,119 INFO  L225             Difference]: With dead ends: 180
[2025-04-28 21:21:43,119 INFO  L226             Difference]: Without dead ends: 180
[2025-04-28 21:21:43,120 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 24 GetRequests, 17 SyntacticMatches, 2 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:43,120 INFO  L437           NwaCegarLoop]: 110 mSDtfsCounter, 9 mSDsluCounter, 39 mSDsCounter, 0 mSdLazyCounter, 153 mSolverCounterSat, 98 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 149 SdHoareTripleChecker+Invalid, 251 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 98 IncrementalHoareTripleChecker+Valid, 153 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,122 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 149 Invalid, 251 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [98 Valid, 153 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:43,122 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 180 states.
[2025-04-28 21:21:43,157 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 180 to 150.
[2025-04-28 21:21:43,158 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 150 states, 45 states have (on average 4.7555555555555555) internal successors, (214), 108 states have internal predecessors, (214), 69 states have call successors, (69), 9 states have call predecessors, (69), 35 states have return successors, (314), 33 states have call predecessors, (314), 69 states have call successors, (314)
[2025-04-28 21:21:43,161 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 150 states to 150 states and 597 transitions.
[2025-04-28 21:21:43,161 INFO  L79                 Accepts]: Start accepts. Automaton has 150 states and 597 transitions. Word has length 17
[2025-04-28 21:21:43,162 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,162 INFO  L485      AbstractCegarLoop]: Abstraction has 150 states and 597 transitions.
[2025-04-28 21:21:43,162 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:43,162 INFO  L278                IsEmpty]: Start isEmpty. Operand 150 states and 597 transitions.
[2025-04-28 21:21:43,169 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:43,169 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,169 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,174 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:43,370 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable13
[2025-04-28 21:21:43,371 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,371 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,371 INFO  L85        PathProgramCache]: Analyzing trace with hash 199095586, now seen corresponding path program 1 times
[2025-04-28 21:21:43,371 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,371 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [345731857]
[2025-04-28 21:21:43,371 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,371 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,379 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:43,390 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:43,390 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,390 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,441 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:43,442 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,442 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [345731857]
[2025-04-28 21:21:43,442 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [345731857] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,442 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,442 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:43,442 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [222473561]
[2025-04-28 21:21:43,442 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,442 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:43,442 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,443 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:43,443 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:43,443 INFO  L87              Difference]: Start difference. First operand 150 states and 597 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:43,798 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,798 INFO  L93              Difference]: Finished difference Result 190 states and 745 transitions.
[2025-04-28 21:21:43,798 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:43,798 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:43,799 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,804 INFO  L225             Difference]: With dead ends: 190
[2025-04-28 21:21:43,804 INFO  L226             Difference]: Without dead ends: 174
[2025-04-28 21:21:43,804 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:43,805 INFO  L437           NwaCegarLoop]: 101 mSDtfsCounter, 11 mSDsluCounter, 54 mSDsCounter, 0 mSdLazyCounter, 205 mSolverCounterSat, 59 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 56 SdHoareTripleChecker+Valid, 155 SdHoareTripleChecker+Invalid, 264 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 59 IncrementalHoareTripleChecker+Valid, 205 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,805 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [56 Valid, 155 Invalid, 264 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [59 Valid, 205 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:43,806 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 174 states.
[2025-04-28 21:21:43,841 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 174 to 142.
[2025-04-28 21:21:43,842 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 142 states, 41 states have (on average 5.512195121951219) internal successors, (226), 105 states have internal predecessors, (226), 70 states have call successors, (70), 10 states have call predecessors, (70), 30 states have return successors, (217), 29 states have call predecessors, (217), 70 states have call successors, (217)
[2025-04-28 21:21:43,845 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 142 states to 142 states and 513 transitions.
[2025-04-28 21:21:43,845 INFO  L79                 Accepts]: Start accepts. Automaton has 142 states and 513 transitions. Word has length 17
[2025-04-28 21:21:43,846 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,846 INFO  L485      AbstractCegarLoop]: Abstraction has 142 states and 513 transitions.
[2025-04-28 21:21:43,846 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:43,847 INFO  L278                IsEmpty]: Start isEmpty. Operand 142 states and 513 transitions.
[2025-04-28 21:21:43,852 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:43,852 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,852 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,852 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:43,852 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,853 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,853 INFO  L85        PathProgramCache]: Analyzing trace with hash 447054141, now seen corresponding path program 1 times
[2025-04-28 21:21:43,853 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,854 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [852124179]
[2025-04-28 21:21:43,854 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,854 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,860 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:43,865 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:43,865 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,866 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,924 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:43,924 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,924 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [852124179]
[2025-04-28 21:21:43,924 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [852124179] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,924 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,924 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:43,924 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1785247689]
[2025-04-28 21:21:43,924 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,925 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:43,925 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,925 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:43,925 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:43,925 INFO  L87              Difference]: Start difference. First operand 142 states and 513 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:44,250 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,250 INFO  L93              Difference]: Finished difference Result 180 states and 579 transitions.
[2025-04-28 21:21:44,250 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:44,251 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:44,251 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,255 INFO  L225             Difference]: With dead ends: 180
[2025-04-28 21:21:44,255 INFO  L226             Difference]: Without dead ends: 146
[2025-04-28 21:21:44,255 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:44,256 INFO  L437           NwaCegarLoop]: 103 mSDtfsCounter, 2 mSDsluCounter, 37 mSDsCounter, 0 mSdLazyCounter, 120 mSolverCounterSat, 109 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 140 SdHoareTripleChecker+Invalid, 229 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 109 IncrementalHoareTripleChecker+Valid, 120 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,256 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 140 Invalid, 229 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [109 Valid, 120 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:44,256 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 146 states.
[2025-04-28 21:21:44,271 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 146 to 106.
[2025-04-28 21:21:44,271 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 106 states, 31 states have (on average 6.580645161290323) internal successors, (204), 79 states have internal predecessors, (204), 55 states have call successors, (55), 11 states have call predecessors, (55), 19 states have return successors, (111), 19 states have call predecessors, (111), 55 states have call successors, (111)
[2025-04-28 21:21:44,273 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 106 states to 106 states and 370 transitions.
[2025-04-28 21:21:44,273 INFO  L79                 Accepts]: Start accepts. Automaton has 106 states and 370 transitions. Word has length 17
[2025-04-28 21:21:44,273 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,273 INFO  L485      AbstractCegarLoop]: Abstraction has 106 states and 370 transitions.
[2025-04-28 21:21:44,274 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 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:44,274 INFO  L278                IsEmpty]: Start isEmpty. Operand 106 states and 370 transitions.
[2025-04-28 21:21:44,277 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:44,277 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,277 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,278 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:21:44,278 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,278 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,278 INFO  L85        PathProgramCache]: Analyzing trace with hash 1709914975, now seen corresponding path program 1 times
[2025-04-28 21:21:44,278 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,278 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [3577197]
[2025-04-28 21:21:44,279 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,279 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,282 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:44,287 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:44,287 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,288 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,399 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:44,399 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,399 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [3577197]
[2025-04-28 21:21:44,399 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [3577197] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,399 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,399 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:44,399 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1187134522]
[2025-04-28 21:21:44,399 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,400 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:44,400 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,400 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:44,400 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:44,400 INFO  L87              Difference]: Start difference. First operand 106 states and 370 transitions. Second operand  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:44,887 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,888 INFO  L93              Difference]: Finished difference Result 120 states and 385 transitions.
[2025-04-28 21:21:44,888 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:44,888 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 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:44,888 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,890 INFO  L225             Difference]: With dead ends: 120
[2025-04-28 21:21:44,890 INFO  L226             Difference]: Without dead ends: 93
[2025-04-28 21:21:44,890 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=22, Invalid=34, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:44,891 INFO  L437           NwaCegarLoop]: 69 mSDtfsCounter, 3 mSDsluCounter, 18 mSDsCounter, 0 mSdLazyCounter, 295 mSolverCounterSat, 50 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 87 SdHoareTripleChecker+Invalid, 345 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 50 IncrementalHoareTripleChecker+Valid, 295 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,891 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 87 Invalid, 345 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [50 Valid, 295 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:44,892 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 93 states.
[2025-04-28 21:21:44,900 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 93 to 71.
[2025-04-28 21:21:44,900 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 71 states, 22 states have (on average 4.5) internal successors, (99), 53 states have internal predecessors, (99), 34 states have call successors, (34), 7 states have call predecessors, (34), 14 states have return successors, (61), 14 states have call predecessors, (61), 34 states have call successors, (61)
[2025-04-28 21:21:44,901 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 71 states to 71 states and 194 transitions.
[2025-04-28 21:21:44,901 INFO  L79                 Accepts]: Start accepts. Automaton has 71 states and 194 transitions. Word has length 17
[2025-04-28 21:21:44,902 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,902 INFO  L485      AbstractCegarLoop]: Abstraction has 71 states and 194 transitions.
[2025-04-28 21:21:44,902 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:44,902 INFO  L278                IsEmpty]: Start isEmpty. Operand 71 states and 194 transitions.
[2025-04-28 21:21:44,904 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:44,904 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,904 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,904 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:21:44,904 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,905 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,905 INFO  L85        PathProgramCache]: Analyzing trace with hash 1692083234, now seen corresponding path program 1 times
[2025-04-28 21:21:44,905 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,905 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1925659292]
[2025-04-28 21:21:44,905 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,905 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,908 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:44,912 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:44,913 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,913 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,076 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:45,076 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,076 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1925659292]
[2025-04-28 21:21:45,076 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1925659292] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,076 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,076 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:45,076 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [721650300]
[2025-04-28 21:21:45,077 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,077 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:45,077 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,077 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:45,077 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:45,078 INFO  L87              Difference]: Start difference. First operand 71 states and 194 transitions. Second operand  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:45,317 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,317 INFO  L93              Difference]: Finished difference Result 91 states and 249 transitions.
[2025-04-28 21:21:45,318 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:45,318 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 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:45,318 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,320 INFO  L225             Difference]: With dead ends: 91
[2025-04-28 21:21:45,320 INFO  L226             Difference]: Without dead ends: 90
[2025-04-28 21:21:45,320 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:45,321 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 1 mSDsluCounter, 26 mSDsCounter, 0 mSdLazyCounter, 194 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 68 SdHoareTripleChecker+Invalid, 200 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 194 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,321 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 68 Invalid, 200 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 194 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:45,321 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-04-28 21:21:45,328 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 70.
[2025-04-28 21:21:45,328 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 70 states, 22 states have (on average 4.2727272727272725) internal successors, (94), 52 states have internal predecessors, (94), 33 states have call successors, (33), 7 states have call predecessors, (33), 14 states have return successors, (60), 14 states have call predecessors, (60), 33 states have call successors, (60)
[2025-04-28 21:21:45,329 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 187 transitions.
[2025-04-28 21:21:45,330 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 187 transitions. Word has length 17
[2025-04-28 21:21:45,330 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,330 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 187 transitions.
[2025-04-28 21:21:45,330 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:45,331 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 187 transitions.
[2025-04-28 21:21:45,333 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:45,334 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,334 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,334 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:21:45,334 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,335 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,335 INFO  L85        PathProgramCache]: Analyzing trace with hash 601358017, now seen corresponding path program 1 times
[2025-04-28 21:21:45,335 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,335 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [465416212]
[2025-04-28 21:21:45,335 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,335 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,341 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:45,364 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:45,368 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,369 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,515 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:45,515 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,515 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [465416212]
[2025-04-28 21:21:45,515 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [465416212] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,515 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [591429610]
[2025-04-28 21:21:45,516 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,516 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,518 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,520 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:45,523 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,566 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:45,580 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:45,580 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,580 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,582 INFO  L256         TraceCheckSpWp]: Trace formula consists of 102 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,583 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:45,690 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:45,690 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,136 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:46,136 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [591429610] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,136 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,136 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 14
[2025-04-28 21:21:46,136 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2136863576]
[2025-04-28 21:21:46,136 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,137 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:46,137 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,137 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:46,138 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=145, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:46,138 INFO  L87              Difference]: Start difference. First operand 70 states and 187 transitions. Second operand  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:46,918 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,918 INFO  L93              Difference]: Finished difference Result 148 states and 378 transitions.
[2025-04-28 21:21:46,919 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 19 states. 
[2025-04-28 21:21:46,919 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10) Word has length 17
[2025-04-28 21:21:46,919 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,921 INFO  L225             Difference]: With dead ends: 148
[2025-04-28 21:21:46,922 INFO  L226             Difference]: Without dead ends: 148
[2025-04-28 21:21:46,922 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 48 GetRequests, 29 SyntacticMatches, 0 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 51 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=95, Invalid=325, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:46,923 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 9 mSDsluCounter, 115 mSDsCounter, 0 mSdLazyCounter, 595 mSolverCounterSat, 51 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 157 SdHoareTripleChecker+Invalid, 646 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 51 IncrementalHoareTripleChecker+Valid, 595 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,923 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 157 Invalid, 646 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [51 Valid, 595 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:46,923 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 148 states.
[2025-04-28 21:21:46,933 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 148 to 70.
[2025-04-28 21:21:46,933 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 70 states, 22 states have (on average 4.2727272727272725) internal successors, (94), 52 states have internal predecessors, (94), 33 states have call successors, (33), 7 states have call predecessors, (33), 14 states have return successors, (60), 14 states have call predecessors, (60), 33 states have call successors, (60)
[2025-04-28 21:21:46,934 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 187 transitions.
[2025-04-28 21:21:46,935 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 187 transitions. Word has length 17
[2025-04-28 21:21:46,935 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,935 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 187 transitions.
[2025-04-28 21:21:46,935 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:46,935 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 187 transitions.
[2025-04-28 21:21:46,942 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:46,943 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,943 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,949 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:21:47,147 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,147 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,148 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,148 INFO  L85        PathProgramCache]: Analyzing trace with hash -918396531, now seen corresponding path program 1 times
[2025-04-28 21:21:47,148 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,148 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [966546330]
[2025-04-28 21:21:47,148 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,148 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,152 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:47,163 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:47,164 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,164 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,273 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:47,273 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,273 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [966546330]
[2025-04-28 21:21:47,273 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [966546330] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,273 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1461073627]
[2025-04-28 21:21:47,274 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,274 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,276 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,278 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:47,281 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,321 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:47,336 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:47,336 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,337 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,338 INFO  L256         TraceCheckSpWp]: Trace formula consists of 104 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,339 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,437 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:47,438 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,894 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:47,895 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1461073627] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,895 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,895 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 14
[2025-04-28 21:21:47,895 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [524504125]
[2025-04-28 21:21:47,895 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,896 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:47,896 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,896 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:47,896 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=145, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:47,896 INFO  L87              Difference]: Start difference. First operand 70 states and 187 transitions. Second operand  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:48,666 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,666 INFO  L93              Difference]: Finished difference Result 148 states and 371 transitions.
[2025-04-28 21:21:48,667 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 20 states. 
[2025-04-28 21:21:48,667 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10) Word has length 17
[2025-04-28 21:21:48,667 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,669 INFO  L225             Difference]: With dead ends: 148
[2025-04-28 21:21:48,669 INFO  L226             Difference]: Without dead ends: 148
[2025-04-28 21:21:48,670 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 29 SyntacticMatches, 0 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 64 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=98, Invalid=364, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:48,670 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 9 mSDsluCounter, 124 mSDsCounter, 0 mSdLazyCounter, 532 mSolverCounterSat, 77 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 166 SdHoareTripleChecker+Invalid, 609 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 77 IncrementalHoareTripleChecker+Valid, 532 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,671 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 166 Invalid, 609 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [77 Valid, 532 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:48,672 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 148 states.
[2025-04-28 21:21:48,681 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 148 to 70.
[2025-04-28 21:21:48,682 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 70 states, 22 states have (on average 4.2727272727272725) internal successors, (94), 52 states have internal predecessors, (94), 33 states have call successors, (33), 7 states have call predecessors, (33), 14 states have return successors, (60), 14 states have call predecessors, (60), 33 states have call successors, (60)
[2025-04-28 21:21:48,683 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 187 transitions.
[2025-04-28 21:21:48,683 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 187 transitions. Word has length 17
[2025-04-28 21:21:48,683 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,684 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 187 transitions.
[2025-04-28 21:21:48,684 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:48,684 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 187 transitions.
[2025-04-28 21:21:48,685 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:48,685 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,686 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,691 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:48,886 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,886 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,887 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,887 INFO  L85        PathProgramCache]: Analyzing trace with hash 1765533855, now seen corresponding path program 1 times
[2025-04-28 21:21:48,887 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,887 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [884189858]
[2025-04-28 21:21:48,887 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,887 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,891 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:48,897 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:48,897 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,897 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,005 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:49,005 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,005 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [884189858]
[2025-04-28 21:21:49,005 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [884189858] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,005 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,005 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:49,006 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2133143486]
[2025-04-28 21:21:49,006 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,006 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:49,006 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,006 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:49,006 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:49,007 INFO  L87              Difference]: Start difference. First operand 70 states and 187 transitions. Second operand  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:49,253 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,253 INFO  L93              Difference]: Finished difference Result 90 states and 241 transitions.
[2025-04-28 21:21:49,253 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:49,254 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 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:49,254 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,255 INFO  L225             Difference]: With dead ends: 90
[2025-04-28 21:21:49,255 INFO  L226             Difference]: Without dead ends: 88
[2025-04-28 21:21:49,256 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:49,256 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 1 mSDsluCounter, 26 mSDsCounter, 0 mSdLazyCounter, 179 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 66 SdHoareTripleChecker+Invalid, 187 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 179 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,256 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 66 Invalid, 187 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 179 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:49,259 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 88 states.
[2025-04-28 21:21:49,264 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 88 to 68.
[2025-04-28 21:21:49,265 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 68 states, 22 states have (on average 3.8181818181818183) internal successors, (84), 50 states have internal predecessors, (84), 31 states have call successors, (31), 7 states have call predecessors, (31), 14 states have return successors, (58), 14 states have call predecessors, (58), 31 states have call successors, (58)
[2025-04-28 21:21:49,265 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 68 states to 68 states and 173 transitions.
[2025-04-28 21:21:49,266 INFO  L79                 Accepts]: Start accepts. Automaton has 68 states and 173 transitions. Word has length 17
[2025-04-28 21:21:49,266 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,266 INFO  L485      AbstractCegarLoop]: Abstraction has 68 states and 173 transitions.
[2025-04-28 21:21:49,266 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:49,266 INFO  L278                IsEmpty]: Start isEmpty. Operand 68 states and 173 transitions.
[2025-04-28 21:21:49,267 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:49,268 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,268 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,268 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-04-28 21:21:49,268 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,268 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,268 INFO  L85        PathProgramCache]: Analyzing trace with hash 19270098, now seen corresponding path program 1 times
[2025-04-28 21:21:49,268 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,269 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1812578640]
[2025-04-28 21:21:49,269 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,269 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,273 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:49,281 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:49,281 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,281 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,428 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:49,428 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,428 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1812578640]
[2025-04-28 21:21:49,428 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1812578640] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,428 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,429 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:49,429 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1773113182]
[2025-04-28 21:21:49,429 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,429 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:49,429 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,429 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:49,430 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:49,430 INFO  L87              Difference]: Start difference. First operand 68 states and 173 transitions. Second operand  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:49,747 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,747 INFO  L93              Difference]: Finished difference Result 98 states and 253 transitions.
[2025-04-28 21:21:49,748 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:49,748 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 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:49,748 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,749 INFO  L225             Difference]: With dead ends: 98
[2025-04-28 21:21:49,749 INFO  L226             Difference]: Without dead ends: 97
[2025-04-28 21:21:49,750 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=27, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:49,750 INFO  L437           NwaCegarLoop]: 37 mSDtfsCounter, 3 mSDsluCounter, 19 mSDsCounter, 0 mSdLazyCounter, 201 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 56 SdHoareTripleChecker+Invalid, 222 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 201 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,750 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 56 Invalid, 222 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 201 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:49,751 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 97 states.
[2025-04-28 21:21:49,756 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 97 to 65.
[2025-04-28 21:21:49,756 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 65 states, 21 states have (on average 3.7142857142857144) internal successors, (78), 48 states have internal predecessors, (78), 30 states have call successors, (30), 7 states have call predecessors, (30), 13 states have return successors, (54), 14 states have call predecessors, (54), 30 states have call successors, (54)
[2025-04-28 21:21:49,757 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 65 states to 65 states and 162 transitions.
[2025-04-28 21:21:49,757 INFO  L79                 Accepts]: Start accepts. Automaton has 65 states and 162 transitions. Word has length 17
[2025-04-28 21:21:49,757 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,758 INFO  L485      AbstractCegarLoop]: Abstraction has 65 states and 162 transitions.
[2025-04-28 21:21:49,758 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:49,758 INFO  L278                IsEmpty]: Start isEmpty. Operand 65 states and 162 transitions.
[2025-04-28 21:21:49,759 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:49,759 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,759 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,759 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-04-28 21:21:49,760 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,760 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,760 INFO  L85        PathProgramCache]: Analyzing trace with hash -1426676098, now seen corresponding path program 1 times
[2025-04-28 21:21:49,760 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,760 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [804272747]
[2025-04-28 21:21:49,760 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,760 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,763 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:49,768 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:49,770 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,770 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,812 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:49,812 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,812 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [804272747]
[2025-04-28 21:21:49,812 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [804272747] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,813 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,813 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:49,813 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1198613273]
[2025-04-28 21:21:49,813 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,813 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:49,813 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,814 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:49,814 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:49,814 INFO  L87              Difference]: Start difference. First operand 65 states and 162 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:49,919 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,922 INFO  L93              Difference]: Finished difference Result 89 states and 223 transitions.
[2025-04-28 21:21:49,923 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:49,923 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 17
[2025-04-28 21:21:49,923 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,924 INFO  L225             Difference]: With dead ends: 89
[2025-04-28 21:21:49,924 INFO  L226             Difference]: Without dead ends: 89
[2025-04-28 21:21:49,925 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:49,926 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 1 mSDsluCounter, 46 mSDsCounter, 0 mSdLazyCounter, 66 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 88 SdHoareTripleChecker+Invalid, 70 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 66 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,927 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 88 Invalid, 70 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 66 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:49,927 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 89 states.
[2025-04-28 21:21:49,931 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 89 to 67.
[2025-04-28 21:21:49,932 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 67 states, 22 states have (on average 3.590909090909091) internal successors, (79), 49 states have internal predecessors, (79), 30 states have call successors, (30), 7 states have call predecessors, (30), 14 states have return successors, (67), 14 states have call predecessors, (67), 30 states have call successors, (67)
[2025-04-28 21:21:49,932 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 67 states to 67 states and 176 transitions.
[2025-04-28 21:21:49,933 INFO  L79                 Accepts]: Start accepts. Automaton has 67 states and 176 transitions. Word has length 17
[2025-04-28 21:21:49,933 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,933 INFO  L485      AbstractCegarLoop]: Abstraction has 67 states and 176 transitions.
[2025-04-28 21:21:49,933 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:49,933 INFO  L278                IsEmpty]: Start isEmpty. Operand 67 states and 176 transitions.
[2025-04-28 21:21:49,934 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:49,935 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,935 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,935 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-04-28 21:21:49,935 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,935 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,935 INFO  L85        PathProgramCache]: Analyzing trace with hash 1127827056, now seen corresponding path program 1 times
[2025-04-28 21:21:49,935 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,936 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [310147365]
[2025-04-28 21:21:49,936 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,936 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,939 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:49,942 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:49,942 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,942 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,047 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:50,048 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,048 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [310147365]
[2025-04-28 21:21:50,048 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [310147365] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,048 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [792280065]
[2025-04-28 21:21:50,048 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,048 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,050 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,052 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:50,056 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,094 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:50,108 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:50,108 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,108 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,109 INFO  L256         TraceCheckSpWp]: Trace formula consists of 100 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,110 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,165 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:50,165 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,064 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:51,064 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [792280065] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,064 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,064 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 11
[2025-04-28 21:21:51,064 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [672501866]
[2025-04-28 21:21:51,064 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,064 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:51,064 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,065 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:51,065 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=82, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:51,065 INFO  L87              Difference]: Start difference. First operand 67 states and 176 transitions. Second operand  has 11 states, 5 states have (on average 2.4) internal successors, (12), 10 states have internal predecessors, (12), 7 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:51,690 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,690 INFO  L93              Difference]: Finished difference Result 119 states and 294 transitions.
[2025-04-28 21:21:51,691 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:51,691 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 5 states have (on average 2.4) internal successors, (12), 10 states have internal predecessors, (12), 7 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 7 states have call successors, (7) Word has length 17
[2025-04-28 21:21:51,691 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,693 INFO  L225             Difference]: With dead ends: 119
[2025-04-28 21:21:51,693 INFO  L226             Difference]: Without dead ends: 107
[2025-04-28 21:21:51,693 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 47 GetRequests, 29 SyntacticMatches, 3 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 16 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=80, Invalid=192, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:51,694 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 18 mSDsluCounter, 74 mSDsCounter, 0 mSdLazyCounter, 473 mSolverCounterSat, 66 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 32 SdHoareTripleChecker+Valid, 114 SdHoareTripleChecker+Invalid, 539 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 66 IncrementalHoareTripleChecker+Valid, 473 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,695 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [32 Valid, 114 Invalid, 539 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [66 Valid, 473 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:51,695 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 107 states.
[2025-04-28 21:21:51,700 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 107 to 71.
[2025-04-28 21:21:51,701 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 71 states, 24 states have (on average 3.6666666666666665) internal successors, (88), 52 states have internal predecessors, (88), 31 states have call successors, (31), 8 states have call predecessors, (31), 15 states have return successors, (65), 15 states have call predecessors, (65), 31 states have call successors, (65)
[2025-04-28 21:21:51,702 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 71 states to 71 states and 184 transitions.
[2025-04-28 21:21:51,702 INFO  L79                 Accepts]: Start accepts. Automaton has 71 states and 184 transitions. Word has length 17
[2025-04-28 21:21:51,702 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,702 INFO  L485      AbstractCegarLoop]: Abstraction has 71 states and 184 transitions.
[2025-04-28 21:21:51,702 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 5 states have (on average 2.4) internal successors, (12), 10 states have internal predecessors, (12), 7 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:51,702 INFO  L278                IsEmpty]: Start isEmpty. Operand 71 states and 184 transitions.
[2025-04-28 21:21:51,703 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:51,704 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,704 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,709 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Ended with exit code 0
[2025-04-28 21:21:51,908 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable23
[2025-04-28 21:21:51,908 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,908 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,908 INFO  L85        PathProgramCache]: Analyzing trace with hash 648231081, now seen corresponding path program 1 times
[2025-04-28 21:21:51,909 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,909 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1528395353]
[2025-04-28 21:21:51,909 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,909 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,912 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:51,918 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:51,918 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,918 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,957 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:51,957 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,957 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1528395353]
[2025-04-28 21:21:51,957 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1528395353] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,958 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,958 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:51,958 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2103199360]
[2025-04-28 21:21:51,958 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,958 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:51,958 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,959 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:51,959 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:51,959 INFO  L87              Difference]: Start difference. First operand 71 states and 184 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:52,053 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,054 INFO  L93              Difference]: Finished difference Result 95 states and 232 transitions.
[2025-04-28 21:21:52,054 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:52,054 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 17
[2025-04-28 21:21:52,055 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,057 INFO  L225             Difference]: With dead ends: 95
[2025-04-28 21:21:52,057 INFO  L226             Difference]: Without dead ends: 95
[2025-04-28 21:21:52,057 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:52,058 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 1 mSDsluCounter, 46 mSDsCounter, 0 mSdLazyCounter, 62 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 89 SdHoareTripleChecker+Invalid, 67 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 62 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,058 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 89 Invalid, 67 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 62 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:52,059 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 95 states.
[2025-04-28 21:21:52,064 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 95 to 71.
[2025-04-28 21:21:52,064 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 71 states, 24 states have (on average 3.6666666666666665) internal successors, (88), 52 states have internal predecessors, (88), 31 states have call successors, (31), 8 states have call predecessors, (31), 15 states have return successors, (61), 15 states have call predecessors, (61), 31 states have call successors, (61)
[2025-04-28 21:21:52,065 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 71 states to 71 states and 180 transitions.
[2025-04-28 21:21:52,065 INFO  L79                 Accepts]: Start accepts. Automaton has 71 states and 180 transitions. Word has length 17
[2025-04-28 21:21:52,066 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,066 INFO  L485      AbstractCegarLoop]: Abstraction has 71 states and 180 transitions.
[2025-04-28 21:21:52,066 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:52,066 INFO  L278                IsEmpty]: Start isEmpty. Operand 71 states and 180 transitions.
[2025-04-28 21:21:52,068 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:52,069 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,069 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,069 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable24
[2025-04-28 21:21:52,069 INFO  L403      AbstractCegarLoop]: === Iteration 25 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,070 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,070 INFO  L85        PathProgramCache]: Analyzing trace with hash -1347425862, now seen corresponding path program 1 times
[2025-04-28 21:21:52,070 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,070 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [53541459]
[2025-04-28 21:21:52,070 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,070 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,073 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:52,082 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:52,083 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,083 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,162 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:52,162 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,162 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [53541459]
[2025-04-28 21:21:52,163 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [53541459] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,163 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1933791784]
[2025-04-28 21:21:52,163 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,163 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,165 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,167 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,170 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,213 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:52,227 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:52,227 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,227 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,228 INFO  L256         TraceCheckSpWp]: Trace formula consists of 99 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,229 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,313 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:52,313 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,716 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:52,716 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1933791784] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,717 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,717 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 14
[2025-04-28 21:21:52,717 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1734158793]
[2025-04-28 21:21:52,717 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,717 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:52,717 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,718 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:52,718 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=39, Invalid=143, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:52,718 INFO  L87              Difference]: Start difference. First operand 71 states and 180 transitions. Second operand  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
