./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/ultimate/Lia-NonLinArrays/29_conditionals_vs_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:25:34,675 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:25:34,713 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a4941720-3a0b-44d0-8842-39fe9152cf4f/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:25:34,716 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:25:34,716 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:25:34,730 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:25:34,730 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:25:34,730 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:25:34,730 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:25:34,730 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:25:34,730 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:25:34,731 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:25:34,731 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:34,731 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:25:34,731 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:25:34,732 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:25:34,732 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:25:34,913 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:25:34,920 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:25:34,922 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:25:34,923 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:25:34,923 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:25:34,924 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a4941720-3a0b-44d0-8842-39fe9152cf4f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/ultimate/Lia-NonLinArrays/29_conditionals_vs_000.smt2
[2025-05-07 17:25:34,925 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:25:34,928 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:25:35,230 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a4941720-3a0b-44d0-8842-39fe9152cf4f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/ultimate/Lia-NonLinArrays/29_conditionals_vs_000.smt2
[2025-05-07 17:25:35,233 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:25:35,234 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:25:35,234 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:25:35,235 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:25:35,235 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:25:35,237 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,263 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35 Unit
[2025-05-07 17:25:35,263 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:25:35,264 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:25:35,264 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:25:35,264 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:25:35,275 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,275 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,296 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,296 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,304 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,306 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,310 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,312 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,313 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,325 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:25:35,326 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:25:35,326 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:25:35,326 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:25:35,327 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (1/1) ...
[2025-05-07 17:25:35,329 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:35,339 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:35,348 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-05-07 17:25:35,350 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:25:35,358 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:25:35,358 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:25:35,358 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:25:35,358 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Inv given in one single declaration
[2025-05-07 17:25:35,358 INFO  L130     BoogieDeclarations]: Found specification of procedure Inv
[2025-05-07 17:25:35,358 INFO  L138     BoogieDeclarations]: Found implementation of procedure Inv
[2025-05-07 17:25:35,358 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:25:35,358 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:25:35,358 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:25:35,401 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:25:35,403 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:25:35,661 INFO  L?                        ?]: Removed 15 outVars from TransFormulas that were not future-live.
[2025-05-07 17:25:35,661 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:25:35,672 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:25:35,672 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-05-07 17:25:35,673 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:35 BoogieIcfgContainer
[2025-05-07 17:25:35,673 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:25:35,674 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:25:35,674 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:25:35,677 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:25:35,677 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:35" (1/3) ...
[2025-05-07 17:25:35,677 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@42300647 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:25:35, skipping insertion in model container
[2025-05-07 17:25:35,678 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:35" (2/3) ...
[2025-05-07 17:25:35,678 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@42300647 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:25:35, skipping insertion in model container
[2025-05-07 17:25:35,678 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:35" (3/3) ...
[2025-05-07 17:25:35,679 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:25:35,690 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:25:35,691 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 70 locations, 245 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:25:35,726 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:25:35,735 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;@211067f5, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:25:35,736 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:25:35,738 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 70 states, 6 states have (on average 10.333333333333334) internal successors, (62), 62 states have internal predecessors, (62), 61 states have call successors, (61), 2 states have call predecessors, (61), 2 states have return successors, (61), 7 states have call predecessors, (61), 61 states have call successors, (61)
[2025-05-07 17:25:35,769 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-05-07 17:25:35,770 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:35,770 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-05-07 17:25:35,770 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:35,774 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:35,774 INFO  L85        PathProgramCache]: Analyzing trace with hash 417039965, now seen corresponding path program 1 times
[2025-05-07 17:25:35,781 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:35,782 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [162380267]
[2025-05-07 17:25:35,782 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:35,782 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:35,802 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-05-07 17:25:35,804 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-05-07 17:25:35,804 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:35,804 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:35,826 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:35,826 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:35,826 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [162380267]
[2025-05-07 17:25:35,827 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [162380267] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:35,827 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:35,829 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-05-07 17:25:35,830 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1055551842]
[2025-05-07 17:25:35,831 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:35,834 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-05-07 17:25:35,834 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:35,855 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-05-07 17:25:35,856 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-05-07 17:25:35,857 INFO  L87              Difference]: Start difference. First operand  has 70 states, 6 states have (on average 10.333333333333334) internal successors, (62), 62 states have internal predecessors, (62), 61 states have call successors, (61), 2 states have call predecessors, (61), 2 states have return successors, (61), 7 states have call predecessors, (61), 61 states have call successors, (61) Second operand  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-05-07 17:25:35,885 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:35,886 INFO  L93              Difference]: Finished difference Result 68 states and 181 transitions.
[2025-05-07 17:25:35,886 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-05-07 17:25:35,888 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1) Word has length 5
[2025-05-07 17:25:35,888 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:35,899 INFO  L225             Difference]: With dead ends: 68
[2025-05-07 17:25:35,900 INFO  L226             Difference]: Without dead ends: 68
[2025-05-07 17:25:35,901 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-05-07 17:25:35,904 INFO  L437           NwaCegarLoop]: 181 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 181 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:35,904 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 181 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:35,915 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 68 states.
[2025-05-07 17:25:35,958 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 68 to 68.
[2025-05-07 17:25:35,960 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 68 states, 5 states have (on average 11.8) internal successors, (59), 59 states have internal predecessors, (59), 61 states have call successors, (61), 2 states have call predecessors, (61), 2 states have return successors, (61), 7 states have call predecessors, (61), 61 states have call successors, (61)
[2025-05-07 17:25:35,967 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 68 states to 68 states and 181 transitions.
[2025-05-07 17:25:35,968 INFO  L79                 Accepts]: Start accepts. Automaton has 68 states and 181 transitions. Word has length 5
[2025-05-07 17:25:35,968 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:35,968 INFO  L485      AbstractCegarLoop]: Abstraction has 68 states and 181 transitions.
[2025-05-07 17:25:35,969 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-05-07 17:25:35,969 INFO  L278                IsEmpty]: Start isEmpty. Operand 68 states and 181 transitions.
[2025-05-07 17:25:35,984 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-05-07 17:25:35,984 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:35,984 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:35,984 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:25:35,985 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:35,985 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:35,985 INFO  L85        PathProgramCache]: Analyzing trace with hash 1178356151, now seen corresponding path program 1 times
[2025-05-07 17:25:35,986 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:35,986 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1984158312]
[2025-05-07 17:25:35,986 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:35,986 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:35,992 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-05-07 17:25:36,011 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-05-07 17:25:36,012 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:36,012 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:36,077 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:36,078 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:36,078 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1984158312]
[2025-05-07 17:25:36,078 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1984158312] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:36,078 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:36,078 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:36,078 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [443106241]
[2025-05-07 17:25:36,078 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:36,079 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:36,079 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:36,079 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:36,079 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:36,080 INFO  L87              Difference]: Start difference. First operand 68 states and 181 transitions. 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-05-07 17:25:36,759 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:36,759 INFO  L93              Difference]: Finished difference Result 103 states and 339 transitions.
[2025-05-07 17:25:36,759 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:36,760 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-05-07 17:25:36,760 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:36,764 INFO  L225             Difference]: With dead ends: 103
[2025-05-07 17:25:36,764 INFO  L226             Difference]: Without dead ends: 103
[2025-05-07 17:25:36,764 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-05-07 17:25:36,765 INFO  L437           NwaCegarLoop]: 185 mSDtfsCounter, 29 mSDsluCounter, 214 mSDsCounter, 0 mSdLazyCounter, 337 mSolverCounterSat, 86 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 399 SdHoareTripleChecker+Invalid, 423 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 86 IncrementalHoareTripleChecker+Valid, 337 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:36,765 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 399 Invalid, 423 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [86 Valid, 337 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:25:36,766 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 103 states.
[2025-05-07 17:25:36,785 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 103 to 103.
[2025-05-07 17:25:36,786 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 103 states, 7 states have (on average 12.714285714285714) internal successors, (89), 88 states have internal predecessors, (89), 94 states have call successors, (94), 3 states have call predecessors, (94), 3 states have return successors, (156), 12 states have call predecessors, (156), 94 states have call successors, (156)
[2025-05-07 17:25:36,788 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 103 states to 103 states and 339 transitions.
[2025-05-07 17:25:36,788 INFO  L79                 Accepts]: Start accepts. Automaton has 103 states and 339 transitions. Word has length 9
[2025-05-07 17:25:36,789 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:36,789 INFO  L485      AbstractCegarLoop]: Abstraction has 103 states and 339 transitions.
[2025-05-07 17:25:36,789 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-05-07 17:25:36,789 INFO  L278                IsEmpty]: Start isEmpty. Operand 103 states and 339 transitions.
[2025-05-07 17:25:36,796 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-05-07 17:25:36,797 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:36,797 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:36,797 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:25:36,797 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:36,797 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:36,797 INFO  L85        PathProgramCache]: Analyzing trace with hash 772584098, now seen corresponding path program 1 times
[2025-05-07 17:25:36,797 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:36,797 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2019150019]
[2025-05-07 17:25:36,797 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:36,797 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:36,801 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-05-07 17:25:36,808 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-05-07 17:25:36,808 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:36,808 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:36,854 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:36,854 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:36,854 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2019150019]
[2025-05-07 17:25:36,854 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2019150019] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:36,854 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [431634139]
[2025-05-07 17:25:36,854 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:36,855 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:36,857 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:36,858 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:36,860 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:25:36,893 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-05-07 17:25:36,908 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-05-07 17:25:36,908 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:36,908 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:36,909 INFO  L256         TraceCheckSpWp]: Trace formula consists of 126 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:36,913 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:36,945 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:36,945 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:25:37,033 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:37,033 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [431634139] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:25:37,033 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:25:37,034 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 5
[2025-05-07 17:25:37,034 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [595915139]
[2025-05-07 17:25:37,034 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:25:37,034 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:25:37,034 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:37,035 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:25:37,035 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:25:37,035 INFO  L87              Difference]: Start difference. First operand 103 states and 339 transitions. Second operand  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-05-07 17:25:38,608 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:38,608 INFO  L93              Difference]: Finished difference Result 269 states and 1350 transitions.
[2025-05-07 17:25:38,608 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:38,608 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-05-07 17:25:38,608 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:38,627 INFO  L225             Difference]: With dead ends: 269
[2025-05-07 17:25:38,627 INFO  L226             Difference]: Without dead ends: 269
[2025-05-07 17:25:38,627 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 30 GetRequests, 23 SyntacticMatches, 3 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:38,628 INFO  L437           NwaCegarLoop]: 346 mSDtfsCounter, 83 mSDsluCounter, 381 mSDsCounter, 0 mSdLazyCounter, 954 mSolverCounterSat, 298 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 97 SdHoareTripleChecker+Valid, 727 SdHoareTripleChecker+Invalid, 1252 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 298 IncrementalHoareTripleChecker+Valid, 954 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:38,628 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [97 Valid, 727 Invalid, 1252 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [298 Valid, 954 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-05-07 17:25:38,629 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 269 states.
[2025-05-07 17:25:38,723 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 269 to 199.
[2025-05-07 17:25:38,723 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 199 states, 11 states have (on average 15.909090909090908) internal successors, (175), 172 states have internal predecessors, (175), 186 states have call successors, (186), 5 states have call predecessors, (186), 5 states have return successors, (468), 22 states have call predecessors, (468), 186 states have call successors, (468)
[2025-05-07 17:25:38,728 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 199 states to 199 states and 829 transitions.
[2025-05-07 17:25:38,728 INFO  L79                 Accepts]: Start accepts. Automaton has 199 states and 829 transitions. Word has length 12
[2025-05-07 17:25:38,728 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:38,728 INFO  L485      AbstractCegarLoop]: Abstraction has 199 states and 829 transitions.
[2025-05-07 17:25:38,729 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-05-07 17:25:38,729 INFO  L278                IsEmpty]: Start isEmpty. Operand 199 states and 829 transitions.
[2025-05-07 17:25:38,744 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:38,744 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:38,745 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:38,750 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:25:38,945 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:38,946 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:38,948 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:38,948 INFO  L85        PathProgramCache]: Analyzing trace with hash 475407756, now seen corresponding path program 1 times
[2025-05-07 17:25:38,949 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:38,949 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [901237051]
[2025-05-07 17:25:38,949 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:38,949 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:38,954 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:38,963 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:38,963 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:38,963 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:39,051 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:39,051 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:39,052 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [901237051]
[2025-05-07 17:25:39,052 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [901237051] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:39,052 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:39,052 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:39,053 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1706677632]
[2025-05-07 17:25:39,053 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:39,054 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:39,054 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:39,055 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:39,055 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:39,056 INFO  L87              Difference]: Start difference. First operand 199 states and 829 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 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-05-07 17:25:39,510 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:39,510 INFO  L93              Difference]: Finished difference Result 339 states and 1818 transitions.
[2025-05-07 17:25:39,511 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:39,511 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), 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-05-07 17:25:39,511 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:39,549 INFO  L225             Difference]: With dead ends: 339
[2025-05-07 17:25:39,549 INFO  L226             Difference]: Without dead ends: 339
[2025-05-07 17:25:39,549 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-05-07 17:25:39,550 INFO  L437           NwaCegarLoop]: 246 mSDtfsCounter, 29 mSDsluCounter, 272 mSDsCounter, 0 mSdLazyCounter, 348 mSolverCounterSat, 86 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 50 SdHoareTripleChecker+Valid, 518 SdHoareTripleChecker+Invalid, 434 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 86 IncrementalHoareTripleChecker+Valid, 348 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:39,550 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [50 Valid, 518 Invalid, 434 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [86 Valid, 348 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:25:39,551 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 339 states.
[2025-05-07 17:25:39,649 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 339 to 339.
[2025-05-07 17:25:39,650 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 339 states, 19 states have (on average 17.0) internal successors, (323), 288 states have internal predecessors, (323), 318 states have call successors, (318), 9 states have call predecessors, (318), 9 states have return successors, (1177), 42 states have call predecessors, (1177), 318 states have call successors, (1177)
[2025-05-07 17:25:39,658 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 339 states to 339 states and 1818 transitions.
[2025-05-07 17:25:39,659 INFO  L79                 Accepts]: Start accepts. Automaton has 339 states and 1818 transitions. Word has length 13
[2025-05-07 17:25:39,659 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:39,659 INFO  L485      AbstractCegarLoop]: Abstraction has 339 states and 1818 transitions.
[2025-05-07 17:25:39,659 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), 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-05-07 17:25:39,659 INFO  L278                IsEmpty]: Start isEmpty. Operand 339 states and 1818 transitions.
[2025-05-07 17:25:39,668 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:39,668 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:39,668 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:39,668 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:25:39,668 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:39,669 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:39,669 INFO  L85        PathProgramCache]: Analyzing trace with hash -1950436788, now seen corresponding path program 1 times
[2025-05-07 17:25:39,669 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:39,669 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1233794856]
[2025-05-07 17:25:39,669 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:39,669 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:39,672 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:39,674 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:39,674 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:39,674 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:39,695 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:39,695 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:39,695 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1233794856]
[2025-05-07 17:25:39,695 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1233794856] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:39,695 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:39,696 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:39,696 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1762302079]
[2025-05-07 17:25:39,696 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:39,696 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:39,696 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:39,696 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:39,696 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:39,697 INFO  L87              Difference]: Start difference. First operand 339 states and 1818 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 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-05-07 17:25:40,122 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:40,122 INFO  L93              Difference]: Finished difference Result 479 states and 3067 transitions.
[2025-05-07 17:25:40,123 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:40,123 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), 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-05-07 17:25:40,123 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:40,159 INFO  L225             Difference]: With dead ends: 479
[2025-05-07 17:25:40,159 INFO  L226             Difference]: Without dead ends: 479
[2025-05-07 17:25:40,159 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-05-07 17:25:40,160 INFO  L437           NwaCegarLoop]: 246 mSDtfsCounter, 29 mSDsluCounter, 256 mSDsCounter, 0 mSdLazyCounter, 356 mSolverCounterSat, 86 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 58 SdHoareTripleChecker+Valid, 502 SdHoareTripleChecker+Invalid, 442 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 86 IncrementalHoareTripleChecker+Valid, 356 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:40,160 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [58 Valid, 502 Invalid, 442 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [86 Valid, 356 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:25:40,161 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 479 states.
[2025-05-07 17:25:40,342 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 479 to 479.
[2025-05-07 17:25:40,344 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 479 states, 27 states have (on average 18.037037037037038) internal successors, (487), 404 states have internal predecessors, (487), 450 states have call successors, (450), 13 states have call predecessors, (450), 13 states have return successors, (2130), 62 states have call predecessors, (2130), 450 states have call successors, (2130)
[2025-05-07 17:25:40,368 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 479 states to 479 states and 3067 transitions.
[2025-05-07 17:25:40,368 INFO  L79                 Accepts]: Start accepts. Automaton has 479 states and 3067 transitions. Word has length 13
[2025-05-07 17:25:40,368 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:40,368 INFO  L485      AbstractCegarLoop]: Abstraction has 479 states and 3067 transitions.
[2025-05-07 17:25:40,368 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), 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-05-07 17:25:40,368 INFO  L278                IsEmpty]: Start isEmpty. Operand 479 states and 3067 transitions.
[2025-05-07 17:25:40,389 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:40,389 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:40,389 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:40,389 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:25:40,389 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:40,390 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:40,390 INFO  L85        PathProgramCache]: Analyzing trace with hash 2023878321, now seen corresponding path program 1 times
[2025-05-07 17:25:40,390 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:40,390 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1762120207]
[2025-05-07 17:25:40,390 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:40,390 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:40,393 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:40,396 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:40,396 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:40,396 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:40,415 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:40,415 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:40,415 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1762120207]
[2025-05-07 17:25:40,415 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1762120207] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:40,415 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:40,416 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:40,416 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [621465535]
[2025-05-07 17:25:40,416 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:40,416 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:40,416 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:40,417 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:40,417 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:40,417 INFO  L87              Difference]: Start difference. First operand 479 states and 3067 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-05-07 17:25:41,127 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:41,128 INFO  L93              Difference]: Finished difference Result 577 states and 6242 transitions.
[2025-05-07 17:25:41,128 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:41,128 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-05-07 17:25:41,128 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:41,248 INFO  L225             Difference]: With dead ends: 577
[2025-05-07 17:25:41,248 INFO  L226             Difference]: Without dead ends: 577
[2025-05-07 17:25:41,249 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-05-07 17:25:41,249 INFO  L437           NwaCegarLoop]: 192 mSDtfsCounter, 30 mSDsluCounter, 176 mSDsCounter, 0 mSdLazyCounter, 569 mSolverCounterSat, 70 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 52 SdHoareTripleChecker+Valid, 368 SdHoareTripleChecker+Invalid, 639 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 70 IncrementalHoareTripleChecker+Valid, 569 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:41,249 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [52 Valid, 368 Invalid, 639 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [70 Valid, 569 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:25:41,250 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 577 states.
[2025-05-07 17:25:41,685 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 577 to 549.
[2025-05-07 17:25:41,687 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 549 states, 31 states have (on average 17.64516129032258) internal successors, (547), 462 states have internal predecessors, (547), 516 states have call successors, (516), 15 states have call predecessors, (516), 15 states have return successors, (2583), 72 states have call predecessors, (2583), 516 states have call successors, (2583)
[2025-05-07 17:25:41,707 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 549 states to 549 states and 3646 transitions.
[2025-05-07 17:25:41,707 INFO  L79                 Accepts]: Start accepts. Automaton has 549 states and 3646 transitions. Word has length 13
[2025-05-07 17:25:41,707 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:41,707 INFO  L485      AbstractCegarLoop]: Abstraction has 549 states and 3646 transitions.
[2025-05-07 17:25:41,707 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-05-07 17:25:41,707 INFO  L278                IsEmpty]: Start isEmpty. Operand 549 states and 3646 transitions.
[2025-05-07 17:25:41,725 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:41,726 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:41,726 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:41,726 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:25:41,726 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:41,727 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:41,727 INFO  L85        PathProgramCache]: Analyzing trace with hash -642524737, now seen corresponding path program 1 times
[2025-05-07 17:25:41,727 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:41,727 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [264789347]
[2025-05-07 17:25:41,727 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:41,727 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:41,730 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:41,732 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:41,732 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:41,732 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:41,753 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:41,753 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:41,753 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [264789347]
[2025-05-07 17:25:41,753 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [264789347] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:41,753 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:41,754 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:41,754 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [634643560]
[2025-05-07 17:25:41,754 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:41,754 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:41,754 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:41,754 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:41,754 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:41,755 INFO  L87              Difference]: Start difference. First operand 549 states and 3646 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 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-05-07 17:25:42,245 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:42,245 INFO  L93              Difference]: Finished difference Result 689 states and 5173 transitions.
[2025-05-07 17:25:42,246 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:42,246 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), 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-05-07 17:25:42,246 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:42,310 INFO  L225             Difference]: With dead ends: 689
[2025-05-07 17:25:42,310 INFO  L226             Difference]: Without dead ends: 689
[2025-05-07 17:25:42,310 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-05-07 17:25:42,310 INFO  L437           NwaCegarLoop]: 244 mSDtfsCounter, 29 mSDsluCounter, 251 mSDsCounter, 0 mSdLazyCounter, 357 mSolverCounterSat, 86 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 60 SdHoareTripleChecker+Valid, 495 SdHoareTripleChecker+Invalid, 443 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 86 IncrementalHoareTripleChecker+Valid, 357 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:42,310 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [60 Valid, 495 Invalid, 443 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [86 Valid, 357 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:25:42,311 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 689 states.
[2025-05-07 17:25:42,640 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 689 to 689.
[2025-05-07 17:25:42,643 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 689 states, 39 states have (on average 18.28205128205128) internal successors, (713), 578 states have internal predecessors, (713), 648 states have call successors, (648), 19 states have call predecessors, (648), 19 states have return successors, (3812), 92 states have call predecessors, (3812), 648 states have call successors, (3812)
[2025-05-07 17:25:42,668 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 689 states to 689 states and 5173 transitions.
[2025-05-07 17:25:42,668 INFO  L79                 Accepts]: Start accepts. Automaton has 689 states and 5173 transitions. Word has length 13
[2025-05-07 17:25:42,668 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:42,668 INFO  L485      AbstractCegarLoop]: Abstraction has 689 states and 5173 transitions.
[2025-05-07 17:25:42,668 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), 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-05-07 17:25:42,668 INFO  L278                IsEmpty]: Start isEmpty. Operand 689 states and 5173 transitions.
[2025-05-07 17:25:42,686 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-05-07 17:25:42,686 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:42,686 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:42,686 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:25:42,686 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:42,686 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:42,687 INFO  L85        PathProgramCache]: Analyzing trace with hash 978181788, now seen corresponding path program 1 times
[2025-05-07 17:25:42,687 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:42,687 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2130122892]
[2025-05-07 17:25:42,687 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:42,687 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:42,690 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-05-07 17:25:42,692 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-05-07 17:25:42,692 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:42,692 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:42,721 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:25:42,721 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:42,721 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2130122892]
[2025-05-07 17:25:42,721 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2130122892] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:42,721 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [945284279]
[2025-05-07 17:25:42,721 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:42,721 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:42,724 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:42,726 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:42,727 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:25:42,760 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-05-07 17:25:42,781 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-05-07 17:25:42,781 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:42,782 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:42,782 INFO  L256         TraceCheckSpWp]: Trace formula consists of 185 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:42,783 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:42,795 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:25:42,795 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:25:42,897 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:25:42,898 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [945284279] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:25:42,898 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:25:42,898 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-05-07 17:25:42,898 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1303164783]
[2025-05-07 17:25:42,898 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:25:42,898 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:25:42,898 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:42,898 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:25:42,898 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:42,898 INFO  L87              Difference]: Start difference. First operand 689 states and 5173 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:25:45,423 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:45,423 INFO  L93              Difference]: Finished difference Result 761 states and 11499 transitions.
[2025-05-07 17:25:45,423 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:25:45,424 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 16
[2025-05-07 17:25:45,424 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:45,574 INFO  L225             Difference]: With dead ends: 761
[2025-05-07 17:25:45,574 INFO  L226             Difference]: Without dead ends: 761
[2025-05-07 17:25:45,574 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 44 GetRequests, 31 SyntacticMatches, 2 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 20 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=54, Invalid=102, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:25:45,575 INFO  L437           NwaCegarLoop]: 353 mSDtfsCounter, 90 mSDsluCounter, 350 mSDsCounter, 0 mSdLazyCounter, 1758 mSolverCounterSat, 355 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 243 SdHoareTripleChecker+Valid, 703 SdHoareTripleChecker+Invalid, 2113 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 355 IncrementalHoareTripleChecker+Valid, 1758 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:45,575 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [243 Valid, 703 Invalid, 2113 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [355 Valid, 1758 Invalid, 0 Unknown, 0 Unchecked, 2.4s Time]
[2025-05-07 17:25:45,576 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 761 states.
[2025-05-07 17:25:46,093 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 761 to 619.
[2025-05-07 17:25:46,095 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 619 states, 35 states have (on average 18.65714285714286) internal successors, (653), 520 states have internal predecessors, (653), 582 states have call successors, (582), 17 states have call predecessors, (582), 17 states have return successors, (2979), 82 states have call predecessors, (2979), 582 states have call successors, (2979)
[2025-05-07 17:25:46,113 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 619 states to 619 states and 4214 transitions.
[2025-05-07 17:25:46,114 INFO  L79                 Accepts]: Start accepts. Automaton has 619 states and 4214 transitions. Word has length 16
[2025-05-07 17:25:46,114 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:46,114 INFO  L485      AbstractCegarLoop]: Abstraction has 619 states and 4214 transitions.
[2025-05-07 17:25:46,114 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:25:46,114 INFO  L278                IsEmpty]: Start isEmpty. Operand 619 states and 4214 transitions.
[2025-05-07 17:25:46,127 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-05-07 17:25:46,127 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:46,127 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:46,130 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:25:46,327 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:46,327 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:46,328 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:46,328 INFO  L85        PathProgramCache]: Analyzing trace with hash 349304326, now seen corresponding path program 1 times
[2025-05-07 17:25:46,328 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:46,328 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [729986697]
[2025-05-07 17:25:46,328 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:46,329 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:46,332 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-05-07 17:25:46,335 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-05-07 17:25:46,335 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:46,335 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:46,359 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:25:46,359 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:46,359 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [729986697]
[2025-05-07 17:25:46,360 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [729986697] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:46,360 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:46,360 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:46,360 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [559818852]
[2025-05-07 17:25:46,360 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:46,360 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:46,360 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:46,361 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:46,361 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:46,361 INFO  L87              Difference]: Start difference. First operand 619 states and 4214 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-05-07 17:25:47,129 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:47,129 INFO  L93              Difference]: Finished difference Result 947 states and 11786 transitions.
[2025-05-07 17:25:47,130 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:47,130 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-05-07 17:25:47,130 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:47,304 INFO  L225             Difference]: With dead ends: 947
[2025-05-07 17:25:47,304 INFO  L226             Difference]: Without dead ends: 947
[2025-05-07 17:25:47,304 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-05-07 17:25:47,304 INFO  L437           NwaCegarLoop]: 189 mSDtfsCounter, 30 mSDsluCounter, 167 mSDsCounter, 0 mSdLazyCounter, 508 mSolverCounterSat, 103 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 50 SdHoareTripleChecker+Valid, 356 SdHoareTripleChecker+Invalid, 611 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 103 IncrementalHoareTripleChecker+Valid, 508 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:47,304 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [50 Valid, 356 Invalid, 611 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [103 Valid, 508 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-05-07 17:25:47,305 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 947 states.
[2025-05-07 17:25:47,937 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 947 to 899.
[2025-05-07 17:25:47,940 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 899 states, 51 states have (on average 16.686274509803923) internal successors, (851), 752 states have internal predecessors, (851), 846 states have call successors, (846), 25 states have call predecessors, (846), 25 states have return successors, (5033), 122 states have call predecessors, (5033), 846 states have call successors, (5033)
[2025-05-07 17:25:47,973 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 899 states to 899 states and 6730 transitions.
[2025-05-07 17:25:47,973 INFO  L79                 Accepts]: Start accepts. Automaton has 899 states and 6730 transitions. Word has length 17
[2025-05-07 17:25:47,973 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:47,973 INFO  L485      AbstractCegarLoop]: Abstraction has 899 states and 6730 transitions.
[2025-05-07 17:25:47,973 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-05-07 17:25:47,973 INFO  L278                IsEmpty]: Start isEmpty. Operand 899 states and 6730 transitions.
[2025-05-07 17:25:47,993 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-05-07 17:25:47,993 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:47,993 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:47,993 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:25:47,993 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:47,994 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:47,994 INFO  L85        PathProgramCache]: Analyzing trace with hash -1428712749, now seen corresponding path program 1 times
[2025-05-07 17:25:47,994 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:47,994 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [706178215]
[2025-05-07 17:25:47,994 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:47,994 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:47,998 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-05-07 17:25:48,002 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-05-07 17:25:48,002 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:48,002 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:48,034 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:25:48,034 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:48,034 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [706178215]
[2025-05-07 17:25:48,034 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [706178215] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:48,034 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:48,034 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:48,034 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1356569778]
[2025-05-07 17:25:48,034 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:48,034 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:48,034 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:48,035 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:48,035 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:48,035 INFO  L87              Difference]: Start difference. First operand 899 states and 6730 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-05-07 17:25:48,816 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:48,816 INFO  L93              Difference]: Finished difference Result 1095 states and 14104 transitions.
[2025-05-07 17:25:48,817 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:48,817 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-05-07 17:25:48,817 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:49,012 INFO  L225             Difference]: With dead ends: 1095
[2025-05-07 17:25:49,013 INFO  L226             Difference]: Without dead ends: 1095
[2025-05-07 17:25:49,013 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-05-07 17:25:49,013 INFO  L437           NwaCegarLoop]: 189 mSDtfsCounter, 30 mSDsluCounter, 157 mSDsCounter, 0 mSdLazyCounter, 566 mSolverCounterSat, 102 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 71 SdHoareTripleChecker+Valid, 346 SdHoareTripleChecker+Invalid, 668 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 102 IncrementalHoareTripleChecker+Valid, 566 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:49,013 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [71 Valid, 346 Invalid, 668 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [102 Valid, 566 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-05-07 17:25:49,014 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1095 states.
[2025-05-07 17:25:49,857 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1095 to 1039.
[2025-05-07 17:25:49,861 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1039 states, 59 states have (on average 16.050847457627118) internal successors, (947), 868 states have internal predecessors, (947), 978 states have call successors, (978), 29 states have call predecessors, (978), 29 states have return successors, (6076), 142 states have call predecessors, (6076), 978 states have call successors, (6076)
[2025-05-07 17:25:49,899 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1039 states to 1039 states and 8001 transitions.
[2025-05-07 17:25:49,899 INFO  L79                 Accepts]: Start accepts. Automaton has 1039 states and 8001 transitions. Word has length 17
[2025-05-07 17:25:49,899 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:49,899 INFO  L485      AbstractCegarLoop]: Abstraction has 1039 states and 8001 transitions.
[2025-05-07 17:25:49,899 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-05-07 17:25:49,899 INFO  L278                IsEmpty]: Start isEmpty. Operand 1039 states and 8001 transitions.
[2025-05-07 17:25:49,918 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-05-07 17:25:49,918 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:49,918 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:49,918 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:25:49,919 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:49,920 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:49,920 INFO  L85        PathProgramCache]: Analyzing trace with hash 1958613887, now seen corresponding path program 1 times
[2025-05-07 17:25:49,920 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:49,920 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [40500600]
[2025-05-07 17:25:49,920 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:49,920 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:49,923 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-05-07 17:25:49,925 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-05-07 17:25:49,925 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:49,925 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:49,945 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:25:49,945 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:49,945 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [40500600]
[2025-05-07 17:25:49,945 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [40500600] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:49,945 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:49,946 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:49,946 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [11386667]
[2025-05-07 17:25:49,946 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:49,946 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:49,946 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:49,946 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:49,946 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:49,946 INFO  L87              Difference]: Start difference. First operand 1039 states and 8001 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-05-07 17:25:50,760 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:50,760 INFO  L93              Difference]: Finished difference Result 1243 states and 16350 transitions.
[2025-05-07 17:25:50,761 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:50,761 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-05-07 17:25:50,761 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:50,992 INFO  L225             Difference]: With dead ends: 1243
[2025-05-07 17:25:50,992 INFO  L226             Difference]: Without dead ends: 1243
[2025-05-07 17:25:50,992 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-05-07 17:25:50,993 INFO  L437           NwaCegarLoop]: 310 mSDtfsCounter, 29 mSDsluCounter, 265 mSDsCounter, 0 mSdLazyCounter, 370 mSolverCounterSat, 134 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 71 SdHoareTripleChecker+Valid, 575 SdHoareTripleChecker+Invalid, 504 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 134 IncrementalHoareTripleChecker+Valid, 370 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:50,993 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [71 Valid, 575 Invalid, 504 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [134 Valid, 370 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-05-07 17:25:50,994 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1243 states.
[2025-05-07 17:25:51,843 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1243 to 1179.
[2025-05-07 17:25:51,849 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1179 states, 67 states have (on average 15.925373134328359) internal successors, (1067), 984 states have internal predecessors, (1067), 1110 states have call successors, (1110), 33 states have call predecessors, (1110), 33 states have return successors, (7071), 162 states have call predecessors, (7071), 1110 states have call successors, (7071)
[2025-05-07 17:25:51,901 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1179 states to 1179 states and 9248 transitions.
[2025-05-07 17:25:51,901 INFO  L79                 Accepts]: Start accepts. Automaton has 1179 states and 9248 transitions. Word has length 17
[2025-05-07 17:25:51,901 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:51,901 INFO  L485      AbstractCegarLoop]: Abstraction has 1179 states and 9248 transitions.
[2025-05-07 17:25:51,901 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-05-07 17:25:51,901 INFO  L278                IsEmpty]: Start isEmpty. Operand 1179 states and 9248 transitions.
[2025-05-07 17:25:51,922 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-05-07 17:25:51,922 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:51,922 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:51,922 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:25:51,922 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:51,923 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:51,923 INFO  L85        PathProgramCache]: Analyzing trace with hash -1262090315, now seen corresponding path program 1 times
[2025-05-07 17:25:51,923 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:51,923 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [784631399]
[2025-05-07 17:25:51,923 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:51,923 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:51,925 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-05-07 17:25:51,928 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-05-07 17:25:51,928 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:51,928 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:51,949 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:25:51,950 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:51,950 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [784631399]
[2025-05-07 17:25:51,950 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [784631399] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:51,950 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:51,950 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:51,950 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1201180915]
[2025-05-07 17:25:51,950 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:51,950 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:51,950 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:51,951 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:51,951 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:51,951 INFO  L87              Difference]: Start difference. First operand 1179 states and 9248 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-05-07 17:25:52,684 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:52,685 INFO  L93              Difference]: Finished difference Result 1391 states and 19038 transitions.
[2025-05-07 17:25:52,686 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:52,686 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-05-07 17:25:52,686 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:52,965 INFO  L225             Difference]: With dead ends: 1391
[2025-05-07 17:25:52,965 INFO  L226             Difference]: Without dead ends: 1391
[2025-05-07 17:25:52,965 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-05-07 17:25:52,965 INFO  L437           NwaCegarLoop]: 308 mSDtfsCounter, 29 mSDsluCounter, 260 mSDsCounter, 0 mSdLazyCounter, 369 mSolverCounterSat, 134 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 75 SdHoareTripleChecker+Valid, 568 SdHoareTripleChecker+Invalid, 503 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 134 IncrementalHoareTripleChecker+Valid, 369 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:52,966 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [75 Valid, 568 Invalid, 503 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [134 Valid, 369 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:25:52,967 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1391 states.
[2025-05-07 17:25:54,046 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1391 to 1319.
[2025-05-07 17:25:54,050 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1319 states, 75 states have (on average 15.853333333333333) internal successors, (1189), 1100 states have internal predecessors, (1189), 1242 states have call successors, (1242), 37 states have call predecessors, (1242), 37 states have return successors, (8286), 182 states have call predecessors, (8286), 1242 states have call successors, (8286)
[2025-05-07 17:25:54,099 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1319 states to 1319 states and 10717 transitions.
[2025-05-07 17:25:54,099 INFO  L79                 Accepts]: Start accepts. Automaton has 1319 states and 10717 transitions. Word has length 17
[2025-05-07 17:25:54,100 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:54,100 INFO  L485      AbstractCegarLoop]: Abstraction has 1319 states and 10717 transitions.
[2025-05-07 17:25:54,100 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-05-07 17:25:54,100 INFO  L278                IsEmpty]: Start isEmpty. Operand 1319 states and 10717 transitions.
[2025-05-07 17:25:54,125 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-05-07 17:25:54,125 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:54,125 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:54,125 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:25:54,126 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:54,126 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:54,126 INFO  L85        PathProgramCache]: Analyzing trace with hash 768028766, now seen corresponding path program 1 times
[2025-05-07 17:25:54,126 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:54,127 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [925874123]
[2025-05-07 17:25:54,127 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:54,127 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:54,129 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-05-07 17:25:54,131 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-05-07 17:25:54,131 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:54,131 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:54,150 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:25:54,150 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:54,150 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [925874123]
[2025-05-07 17:25:54,150 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [925874123] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:54,150 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:54,150 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:54,150 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [228774434]
[2025-05-07 17:25:54,150 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:54,150 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:54,150 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:54,151 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:54,151 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:54,151 INFO  L87              Difference]: Start difference. First operand 1319 states and 10717 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:25:54,943 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:54,943 INFO  L93              Difference]: Finished difference Result 1539 states and 22034 transitions.
[2025-05-07 17:25:54,944 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:54,944 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-05-07 17:25:54,944 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:55,253 INFO  L225             Difference]: With dead ends: 1539
[2025-05-07 17:25:55,253 INFO  L226             Difference]: Without dead ends: 1539
[2025-05-07 17:25:55,253 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-05-07 17:25:55,253 INFO  L437           NwaCegarLoop]: 190 mSDtfsCounter, 30 mSDsluCounter, 155 mSDsCounter, 0 mSdLazyCounter, 566 mSolverCounterSat, 102 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 79 SdHoareTripleChecker+Valid, 345 SdHoareTripleChecker+Invalid, 668 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 102 IncrementalHoareTripleChecker+Valid, 566 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:55,254 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [79 Valid, 345 Invalid, 668 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [102 Valid, 566 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:25:55,254 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1539 states.
[2025-05-07 17:25:56,477 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1539 to 1459.
[2025-05-07 17:25:56,482 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1459 states, 83 states have (on average 15.891566265060241) internal successors, (1319), 1216 states have internal predecessors, (1319), 1374 states have call successors, (1374), 41 states have call predecessors, (1374), 41 states have return successors, (9651), 202 states have call predecessors, (9651), 1374 states have call successors, (9651)
[2025-05-07 17:25:56,540 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1459 states to 1459 states and 12344 transitions.
[2025-05-07 17:25:56,540 INFO  L79                 Accepts]: Start accepts. Automaton has 1459 states and 12344 transitions. Word has length 21
[2025-05-07 17:25:56,540 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:56,540 INFO  L485      AbstractCegarLoop]: Abstraction has 1459 states and 12344 transitions.
[2025-05-07 17:25:56,541 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:25:56,541 INFO  L278                IsEmpty]: Start isEmpty. Operand 1459 states and 12344 transitions.
[2025-05-07 17:25:56,566 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-05-07 17:25:56,566 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:56,567 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:56,567 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:25:56,567 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:56,568 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:56,568 INFO  L85        PathProgramCache]: Analyzing trace with hash -1552920844, now seen corresponding path program 1 times
[2025-05-07 17:25:56,568 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:56,568 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [778163152]
[2025-05-07 17:25:56,568 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:56,568 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:56,570 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-05-07 17:25:56,573 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-05-07 17:25:56,573 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:56,573 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:56,592 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:25:56,592 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:56,592 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [778163152]
[2025-05-07 17:25:56,592 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [778163152] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:56,592 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:56,592 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:56,592 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1162613894]
[2025-05-07 17:25:56,592 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:56,593 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:56,593 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:56,593 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:56,593 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:56,593 INFO  L87              Difference]: Start difference. First operand 1459 states and 12344 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, (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-05-07 17:25:57,281 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:57,281 INFO  L93              Difference]: Finished difference Result 1613 states and 23316 transitions.
[2025-05-07 17:25:57,281 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:57,281 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, (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 19
[2025-05-07 17:25:57,282 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:57,648 INFO  L225             Difference]: With dead ends: 1613
[2025-05-07 17:25:57,648 INFO  L226             Difference]: Without dead ends: 1613
[2025-05-07 17:25:57,648 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-05-07 17:25:57,648 INFO  L437           NwaCegarLoop]: 236 mSDtfsCounter, 30 mSDsluCounter, 327 mSDsCounter, 0 mSdLazyCounter, 374 mSolverCounterSat, 72 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 48 SdHoareTripleChecker+Valid, 563 SdHoareTripleChecker+Invalid, 446 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 72 IncrementalHoareTripleChecker+Valid, 374 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:57,648 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [48 Valid, 563 Invalid, 446 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [72 Valid, 374 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:25:57,649 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1613 states.
[2025-05-07 17:25:59,083 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1613 to 1529.
[2025-05-07 17:25:59,088 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1529 states, 87 states have (on average 15.850574712643677) internal successors, (1379), 1274 states have internal predecessors, (1379), 1440 states have call successors, (1440), 43 states have call predecessors, (1440), 43 states have return successors, (10228), 212 states have call predecessors, (10228), 1440 states have call successors, (10228)
[2025-05-07 17:25:59,170 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1529 states to 1529 states and 13047 transitions.
[2025-05-07 17:25:59,170 INFO  L79                 Accepts]: Start accepts. Automaton has 1529 states and 13047 transitions. Word has length 19
[2025-05-07 17:25:59,171 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:59,171 INFO  L485      AbstractCegarLoop]: Abstraction has 1529 states and 13047 transitions.
[2025-05-07 17:25:59,171 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, (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-05-07 17:25:59,171 INFO  L278                IsEmpty]: Start isEmpty. Operand 1529 states and 13047 transitions.
[2025-05-07 17:25:59,203 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-05-07 17:25:59,203 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:59,203 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:59,203 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-05-07 17:25:59,203 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:59,204 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:59,204 INFO  L85        PathProgramCache]: Analyzing trace with hash -1194659283, now seen corresponding path program 1 times
[2025-05-07 17:25:59,204 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:59,204 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1269345758]
[2025-05-07 17:25:59,204 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:59,204 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:59,207 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-05-07 17:25:59,209 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-05-07 17:25:59,209 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:59,209 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:59,226 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:25:59,226 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:59,226 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1269345758]
[2025-05-07 17:25:59,226 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1269345758] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:59,226 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:59,226 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:59,226 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1408335734]
[2025-05-07 17:25:59,226 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:59,227 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:59,227 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:59,227 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:59,227 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:59,227 INFO  L87              Difference]: Start difference. First operand 1529 states and 13047 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, (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-05-07 17:25:59,712 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:59,713 INFO  L93              Difference]: Finished difference Result 1533 states and 13526 transitions.
[2025-05-07 17:25:59,713 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:59,713 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, (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 19
[2025-05-07 17:25:59,713 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:59,922 INFO  L225             Difference]: With dead ends: 1533
[2025-05-07 17:25:59,922 INFO  L226             Difference]: Without dead ends: 1533
[2025-05-07 17:25:59,922 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-05-07 17:25:59,923 INFO  L437           NwaCegarLoop]: 250 mSDtfsCounter, 29 mSDsluCounter, 322 mSDsCounter, 0 mSdLazyCounter, 276 mSolverCounterSat, 60 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 37 SdHoareTripleChecker+Valid, 572 SdHoareTripleChecker+Invalid, 336 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 60 IncrementalHoareTripleChecker+Valid, 276 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:59,923 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [37 Valid, 572 Invalid, 336 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [60 Valid, 276 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:25:59,924 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1533 states.
[2025-05-07 17:26:00,625 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1533 to 1529.
[2025-05-07 17:26:00,631 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1529 states, 87 states have (on average 15.850574712643677) internal successors, (1379), 1274 states have internal predecessors, (1379), 1440 states have call successors, (1440), 43 states have call predecessors, (1440), 43 states have return successors, (10225), 212 states have call predecessors, (10225), 1440 states have call successors, (10225)
[2025-05-07 17:26:00,719 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1529 states to 1529 states and 13044 transitions.
[2025-05-07 17:26:00,719 INFO  L79                 Accepts]: Start accepts. Automaton has 1529 states and 13044 transitions. Word has length 19
[2025-05-07 17:26:00,719 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:00,719 INFO  L485      AbstractCegarLoop]: Abstraction has 1529 states and 13044 transitions.
[2025-05-07 17:26:00,719 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, (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-05-07 17:26:00,719 INFO  L278                IsEmpty]: Start isEmpty. Operand 1529 states and 13044 transitions.
[2025-05-07 17:26:00,748 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-05-07 17:26:00,748 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:00,749 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:00,749 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:26:00,749 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:00,749 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:00,749 INFO  L85        PathProgramCache]: Analyzing trace with hash 1609895785, now seen corresponding path program 1 times
[2025-05-07 17:26:00,749 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:00,749 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1735569319]
[2025-05-07 17:26:00,749 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:00,750 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:00,752 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-05-07 17:26:00,754 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-05-07 17:26:00,754 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:00,754 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:00,771 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:26:00,771 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:00,771 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1735569319]
[2025-05-07 17:26:00,771 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1735569319] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:00,772 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:00,772 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:00,772 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1529247346]
[2025-05-07 17:26:00,772 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:00,772 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:00,772 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:00,772 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:00,772 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:00,772 INFO  L87              Difference]: Start difference. First operand 1529 states and 13044 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:26:01,530 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:01,531 INFO  L93              Difference]: Finished difference Result 1761 states and 26560 transitions.
[2025-05-07 17:26:01,531 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:26:01,532 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-05-07 17:26:01,532 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:01,962 INFO  L225             Difference]: With dead ends: 1761
[2025-05-07 17:26:01,962 INFO  L226             Difference]: Without dead ends: 1761
[2025-05-07 17:26:01,962 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-05-07 17:26:01,962 INFO  L437           NwaCegarLoop]: 302 mSDtfsCounter, 29 mSDsluCounter, 245 mSDsCounter, 0 mSdLazyCounter, 372 mSolverCounterSat, 157 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 75 SdHoareTripleChecker+Valid, 547 SdHoareTripleChecker+Invalid, 529 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 157 IncrementalHoareTripleChecker+Valid, 372 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:01,962 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [75 Valid, 547 Invalid, 529 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [157 Valid, 372 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:26:01,963 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1761 states.
[2025-05-07 17:26:03,742 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1761 to 1669.
[2025-05-07 17:26:03,746 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1669 states, 95 states have (on average 15.842105263157896) internal successors, (1505), 1390 states have internal predecessors, (1505), 1572 states have call successors, (1572), 47 states have call predecessors, (1572), 47 states have return successors, (11719), 232 states have call predecessors, (11719), 1572 states have call successors, (11719)
[2025-05-07 17:26:03,814 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1669 states to 1669 states and 14796 transitions.
[2025-05-07 17:26:03,814 INFO  L79                 Accepts]: Start accepts. Automaton has 1669 states and 14796 transitions. Word has length 21
[2025-05-07 17:26:03,814 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:03,814 INFO  L485      AbstractCegarLoop]: Abstraction has 1669 states and 14796 transitions.
[2025-05-07 17:26:03,814 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:26:03,814 INFO  L278                IsEmpty]: Start isEmpty. Operand 1669 states and 14796 transitions.
[2025-05-07 17:26:03,844 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-05-07 17:26:03,844 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:03,844 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:03,844 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:26:03,844 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:03,845 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:03,845 INFO  L85        PathProgramCache]: Analyzing trace with hash 184907814, now seen corresponding path program 1 times
[2025-05-07 17:26:03,845 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:03,845 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1835301554]
[2025-05-07 17:26:03,845 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:03,845 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:03,848 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-05-07 17:26:03,850 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-05-07 17:26:03,850 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:03,850 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:03,865 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:26:03,865 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:03,865 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1835301554]
[2025-05-07 17:26:03,865 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1835301554] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:03,865 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:03,865 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:03,866 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [921491820]
[2025-05-07 17:26:03,866 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:03,866 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:03,866 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:03,866 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:03,866 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:03,866 INFO  L87              Difference]: Start difference. First operand 1669 states and 14796 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:26:04,572 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:04,572 INFO  L93              Difference]: Finished difference Result 1761 states and 25772 transitions.
[2025-05-07 17:26:04,573 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:26:04,573 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-05-07 17:26:04,573 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:04,974 INFO  L225             Difference]: With dead ends: 1761
[2025-05-07 17:26:04,975 INFO  L226             Difference]: Without dead ends: 1761
[2025-05-07 17:26:04,975 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-05-07 17:26:04,975 INFO  L437           NwaCegarLoop]: 197 mSDtfsCounter, 30 mSDsluCounter, 176 mSDsCounter, 0 mSdLazyCounter, 467 mSolverCounterSat, 88 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 59 SdHoareTripleChecker+Valid, 373 SdHoareTripleChecker+Invalid, 555 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 88 IncrementalHoareTripleChecker+Valid, 467 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:04,975 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [59 Valid, 373 Invalid, 555 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [88 Valid, 467 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-05-07 17:26:04,976 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1761 states.
[2025-05-07 17:26:06,611 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1761 to 1669.
[2025-05-07 17:26:06,615 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1669 states, 95 states have (on average 15.8) internal successors, (1501), 1390 states have internal predecessors, (1501), 1572 states have call successors, (1572), 47 states have call predecessors, (1572), 47 states have return successors, (11327), 232 states have call predecessors, (11327), 1572 states have call successors, (11327)
[2025-05-07 17:26:06,682 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1669 states to 1669 states and 14400 transitions.
[2025-05-07 17:26:06,683 INFO  L79                 Accepts]: Start accepts. Automaton has 1669 states and 14400 transitions. Word has length 21
[2025-05-07 17:26:06,683 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:06,683 INFO  L485      AbstractCegarLoop]: Abstraction has 1669 states and 14400 transitions.
[2025-05-07 17:26:06,683 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:26:06,683 INFO  L278                IsEmpty]: Start isEmpty. Operand 1669 states and 14400 transitions.
[2025-05-07 17:26:06,712 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-05-07 17:26:06,712 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:06,712 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:06,712 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:26:06,712 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:06,713 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:06,713 INFO  L85        PathProgramCache]: Analyzing trace with hash 1729949986, now seen corresponding path program 1 times
[2025-05-07 17:26:06,713 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:06,714 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [959937539]
[2025-05-07 17:26:06,714 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:06,714 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:06,717 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-05-07 17:26:06,718 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-05-07 17:26:06,718 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:06,718 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:06,734 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:26:06,734 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:06,734 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [959937539]
[2025-05-07 17:26:06,735 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [959937539] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:06,735 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:06,735 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:06,735 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [566382137]
[2025-05-07 17:26:06,735 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:06,735 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:06,735 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:06,735 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:06,735 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:06,735 INFO  L87              Difference]: Start difference. First operand 1669 states and 14400 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:26:07,700 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:07,700 INFO  L93              Difference]: Finished difference Result 1909 states and 29360 transitions.
[2025-05-07 17:26:07,700 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:26:07,700 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-05-07 17:26:07,701 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:08,187 INFO  L225             Difference]: With dead ends: 1909
[2025-05-07 17:26:08,187 INFO  L226             Difference]: Without dead ends: 1909
[2025-05-07 17:26:08,187 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-05-07 17:26:08,187 INFO  L437           NwaCegarLoop]: 193 mSDtfsCounter, 30 mSDsluCounter, 157 mSDsCounter, 0 mSdLazyCounter, 526 mSolverCounterSat, 102 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 95 SdHoareTripleChecker+Valid, 350 SdHoareTripleChecker+Invalid, 628 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 102 IncrementalHoareTripleChecker+Valid, 526 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:08,187 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [95 Valid, 350 Invalid, 628 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [102 Valid, 526 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:26:08,188 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1909 states.
[2025-05-07 17:26:10,143 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1909 to 1809.
[2025-05-07 17:26:10,148 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1809 states, 103 states have (on average 15.87378640776699) internal successors, (1635), 1506 states have internal predecessors, (1635), 1704 states have call successors, (1704), 51 states have call predecessors, (1704), 51 states have return successors, (12986), 252 states have call predecessors, (12986), 1704 states have call successors, (12986)
[2025-05-07 17:26:10,225 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1809 states to 1809 states and 16325 transitions.
[2025-05-07 17:26:10,226 INFO  L79                 Accepts]: Start accepts. Automaton has 1809 states and 16325 transitions. Word has length 21
[2025-05-07 17:26:10,226 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:10,226 INFO  L485      AbstractCegarLoop]: Abstraction has 1809 states and 16325 transitions.
[2025-05-07 17:26:10,226 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:26:10,226 INFO  L278                IsEmpty]: Start isEmpty. Operand 1809 states and 16325 transitions.
[2025-05-07 17:26:10,259 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-05-07 17:26:10,259 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:10,259 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:10,259 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:26:10,259 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:10,260 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:10,260 INFO  L85        PathProgramCache]: Analyzing trace with hash 449742055, now seen corresponding path program 1 times
[2025-05-07 17:26:10,260 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:10,260 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [675461219]
[2025-05-07 17:26:10,260 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:10,260 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:10,262 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-05-07 17:26:10,264 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-05-07 17:26:10,264 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:10,264 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:10,278 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:26:10,278 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:10,278 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [675461219]
[2025-05-07 17:26:10,278 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [675461219] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:10,278 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:10,278 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:10,278 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [613896547]
[2025-05-07 17:26:10,279 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:10,279 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:10,279 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:10,279 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:10,279 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:10,279 INFO  L87              Difference]: Start difference. First operand 1809 states and 16325 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, (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-05-07 17:26:11,217 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:11,217 INFO  L93              Difference]: Finished difference Result 2413 states and 47834 transitions.
[2025-05-07 17:26:11,218 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:26:11,218 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, (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 19
[2025-05-07 17:26:11,218 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:12,071 INFO  L225             Difference]: With dead ends: 2413
[2025-05-07 17:26:12,071 INFO  L226             Difference]: Without dead ends: 2413
[2025-05-07 17:26:12,071 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-05-07 17:26:12,071 INFO  L437           NwaCegarLoop]: 245 mSDtfsCounter, 28 mSDsluCounter, 234 mSDsCounter, 0 mSdLazyCounter, 490 mSolverCounterSat, 100 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 38 SdHoareTripleChecker+Valid, 479 SdHoareTripleChecker+Invalid, 590 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 100 IncrementalHoareTripleChecker+Valid, 490 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:12,072 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [38 Valid, 479 Invalid, 590 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [100 Valid, 490 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:26:12,073 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 2413 states.
[2025-05-07 17:26:15,075 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 2413 to 2309.
[2025-05-07 17:26:15,085 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 2309 states, 203 states have (on average 9.660098522167488) internal successors, (1961), 1706 states have internal predecessors, (1961), 2104 states have call successors, (2104), 101 states have call predecessors, (2104), 101 states have return successors, (30008), 502 states have call predecessors, (30008), 2104 states have call successors, (30008)
[2025-05-07 17:26:15,289 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2309 states to 2309 states and 34073 transitions.
[2025-05-07 17:26:15,290 INFO  L79                 Accepts]: Start accepts. Automaton has 2309 states and 34073 transitions. Word has length 19
[2025-05-07 17:26:15,290 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:15,290 INFO  L485      AbstractCegarLoop]: Abstraction has 2309 states and 34073 transitions.
[2025-05-07 17:26:15,290 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, (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-05-07 17:26:15,290 INFO  L278                IsEmpty]: Start isEmpty. Operand 2309 states and 34073 transitions.
[2025-05-07 17:26:15,320 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-05-07 17:26:15,320 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:15,320 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:15,320 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:26:15,321 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:15,321 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:15,322 INFO  L85        PathProgramCache]: Analyzing trace with hash 380023011, now seen corresponding path program 1 times
[2025-05-07 17:26:15,322 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:15,322 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [670392540]
[2025-05-07 17:26:15,322 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:15,322 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:15,325 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-05-07 17:26:15,327 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-05-07 17:26:15,327 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:15,327 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:15,342 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:26:15,342 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:15,342 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [670392540]
[2025-05-07 17:26:15,342 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [670392540] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:15,342 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:15,342 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:15,342 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1013873570]
[2025-05-07 17:26:15,343 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:15,343 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:15,343 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:15,343 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:15,343 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:15,343 INFO  L87              Difference]: Start difference. First operand 2309 states and 34073 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, (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-05-07 17:26:16,143 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:16,143 INFO  L93              Difference]: Finished difference Result 2509 states and 63712 transitions.
[2025-05-07 17:26:16,144 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:26:16,144 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, (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 19
[2025-05-07 17:26:16,144 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:17,291 INFO  L225             Difference]: With dead ends: 2509
[2025-05-07 17:26:17,292 INFO  L226             Difference]: Without dead ends: 2509
[2025-05-07 17:26:17,292 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-05-07 17:26:17,292 INFO  L437           NwaCegarLoop]: 276 mSDtfsCounter, 29 mSDsluCounter, 378 mSDsCounter, 0 mSdLazyCounter, 373 mSolverCounterSat, 63 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 38 SdHoareTripleChecker+Valid, 654 SdHoareTripleChecker+Invalid, 436 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 63 IncrementalHoareTripleChecker+Valid, 373 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:17,292 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [38 Valid, 654 Invalid, 436 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [63 Valid, 373 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-05-07 17:26:17,293 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 2509 states.
[2025-05-07 17:26:21,904 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 2509 to 2309.
[2025-05-07 17:26:21,913 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 2309 states, 203 states have (on average 9.660098522167488) internal successors, (1961), 1706 states have internal predecessors, (1961), 2104 states have call successors, (2104), 101 states have call predecessors, (2104), 101 states have return successors, (29774), 502 states have call predecessors, (29774), 2104 states have call successors, (29774)
[2025-05-07 17:26:22,097 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2309 states to 2309 states and 33839 transitions.
[2025-05-07 17:26:22,097 INFO  L79                 Accepts]: Start accepts. Automaton has 2309 states and 33839 transitions. Word has length 19
[2025-05-07 17:26:22,097 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:22,097 INFO  L485      AbstractCegarLoop]: Abstraction has 2309 states and 33839 transitions.
[2025-05-07 17:26:22,098 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, (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-05-07 17:26:22,098 INFO  L278                IsEmpty]: Start isEmpty. Operand 2309 states and 33839 transitions.
[2025-05-07 17:26:22,134 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 23
[2025-05-07 17:26:22,134 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:22,134 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:22,134 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-05-07 17:26:22,134 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:22,135 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:22,135 INFO  L85        PathProgramCache]: Analyzing trace with hash 1722852754, now seen corresponding path program 2 times
[2025-05-07 17:26:22,135 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:22,135 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1233555922]
[2025-05-07 17:26:22,135 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:26:22,135 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:22,139 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 22 statements into 2 equivalence classes.
[2025-05-07 17:26:22,142 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:26:22,142 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:26:22,142 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:22,168 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:26:22,168 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:22,168 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1233555922]
[2025-05-07 17:26:22,168 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1233555922] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:22,168 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1341427387]
[2025-05-07 17:26:22,168 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:26:22,168 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:22,171 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:22,172 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:26:22,173 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:26:22,202 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 22 statements into 2 equivalence classes.
[2025-05-07 17:26:22,223 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:26:22,223 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:26:22,223 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:22,224 INFO  L256         TraceCheckSpWp]: Trace formula consists of 302 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:22,226 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:22,241 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:26:22,242 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:26:22,394 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:26:22,394 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1341427387] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:26:22,394 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:26:22,394 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-05-07 17:26:22,395 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1353598608]
[2025-05-07 17:26:22,395 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:26:22,395 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:22,395 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:22,395 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:22,395 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:22,395 INFO  L87              Difference]: Start difference. First operand 2309 states and 33839 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:26:24,373 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:24,373 INFO  L93              Difference]: Finished difference Result 4516 states and 85613 transitions.
[2025-05-07 17:26:24,374 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:24,374 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 22
[2025-05-07 17:26:24,374 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:26,262 INFO  L225             Difference]: With dead ends: 4516
[2025-05-07 17:26:26,263 INFO  L226             Difference]: Without dead ends: 4516
[2025-05-07 17:26:26,263 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 51 GetRequests, 43 SyntacticMatches, 3 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:26,263 INFO  L437           NwaCegarLoop]: 416 mSDtfsCounter, 84 mSDsluCounter, 555 mSDsCounter, 0 mSdLazyCounter, 1269 mSolverCounterSat, 207 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 94 SdHoareTripleChecker+Valid, 971 SdHoareTripleChecker+Invalid, 1476 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 207 IncrementalHoareTripleChecker+Valid, 1269 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:26,263 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [94 Valid, 971 Invalid, 1476 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [207 Valid, 1269 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-05-07 17:26:26,265 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 4516 states.
[2025-05-07 17:26:33,983 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 4516 to 4516.
[2025-05-07 17:26:34,007 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 4516 states, 399 states have (on average 9.403508771929825) internal successors, (3752), 3325 states have internal predecessors, (3752), 4115 states have call successors, (4115), 199 states have call predecessors, (4115), 199 states have return successors, (77746), 992 states have call predecessors, (77746), 4115 states have call successors, (77746)
[2025-05-07 17:26:34,559 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 4516 states to 4516 states and 85613 transitions.
[2025-05-07 17:26:34,559 INFO  L79                 Accepts]: Start accepts. Automaton has 4516 states and 85613 transitions. Word has length 22
[2025-05-07 17:26:34,559 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:34,559 INFO  L485      AbstractCegarLoop]: Abstraction has 4516 states and 85613 transitions.
[2025-05-07 17:26:34,559 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:26:34,559 INFO  L278                IsEmpty]: Start isEmpty. Operand 4516 states and 85613 transitions.
[2025-05-07 17:26:34,674 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-05-07 17:26:34,674 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:34,674 INFO  L218           NwaCegarLoop]: trace histogram [5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:34,678 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-05-07 17:26:34,875 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:34,876 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:34,881 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:34,881 INFO  L85        PathProgramCache]: Analyzing trace with hash 599153673, now seen corresponding path program 1 times
[2025-05-07 17:26:34,881 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:34,881 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [206687397]
[2025-05-07 17:26:34,881 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:34,882 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:34,894 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-05-07 17:26:34,907 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-05-07 17:26:34,907 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:34,907 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:34,938 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 16 proven. 0 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:26:34,938 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:34,938 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [206687397]
[2025-05-07 17:26:34,938 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [206687397] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:34,938 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:34,938 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:34,938 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [595584912]
[2025-05-07 17:26:34,938 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:34,938 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:34,938 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:34,938 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:34,939 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:34,939 INFO  L87              Difference]: Start difference. First operand 4516 states and 85613 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-05-07 17:26:36,637 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:36,637 INFO  L93              Difference]: Finished difference Result 4738 states and 123618 transitions.
[2025-05-07 17:26:36,637 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:26:36,638 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-05-07 17:26:36,638 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:39,308 INFO  L225             Difference]: With dead ends: 4738
[2025-05-07 17:26:39,308 INFO  L226             Difference]: Without dead ends: 4738
[2025-05-07 17:26:39,308 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-05-07 17:26:39,311 INFO  L437           NwaCegarLoop]: 207 mSDtfsCounter, 30 mSDsluCounter, 180 mSDsCounter, 0 mSdLazyCounter, 471 mSolverCounterSat, 105 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 90 SdHoareTripleChecker+Valid, 387 SdHoareTripleChecker+Invalid, 576 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 105 IncrementalHoareTripleChecker+Valid, 471 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:39,311 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [90 Valid, 387 Invalid, 576 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [105 Valid, 471 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:26:39,313 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 4738 states.
[2025-05-07 17:26:49,380 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 4738 to 4516.
[2025-05-07 17:26:49,405 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 4516 states, 399 states have (on average 9.403508771929825) internal successors, (3752), 3325 states have internal predecessors, (3752), 4115 states have call successors, (4115), 199 states have call predecessors, (4115), 199 states have return successors, (77386), 992 states have call predecessors, (77386), 4115 states have call successors, (77386)
[2025-05-07 17:26:49,980 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 4516 states to 4516 states and 85253 transitions.
[2025-05-07 17:26:49,980 INFO  L79                 Accepts]: Start accepts. Automaton has 4516 states and 85253 transitions. Word has length 24
[2025-05-07 17:26:49,980 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:49,980 INFO  L485      AbstractCegarLoop]: Abstraction has 4516 states and 85253 transitions.
[2025-05-07 17:26:49,980 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 3 states have call predecessors, (6), 3 states have call successors, (6)
[2025-05-07 17:26:49,980 INFO  L278                IsEmpty]: Start isEmpty. Operand 4516 states and 85253 transitions.
[2025-05-07 17:26:50,028 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 23
[2025-05-07 17:26:50,028 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:50,028 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:50,028 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-05-07 17:26:50,029 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:50,029 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:50,030 INFO  L85        PathProgramCache]: Analyzing trace with hash -1747101276, now seen corresponding path program 1 times
[2025-05-07 17:26:50,030 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:50,030 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [572947671]
[2025-05-07 17:26:50,030 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:50,030 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:50,033 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 22 statements into 1 equivalence classes.
[2025-05-07 17:26:50,035 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:26:50,035 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:50,035 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:50,057 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:26:50,057 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:50,058 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [572947671]
[2025-05-07 17:26:50,058 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [572947671] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:50,058 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [530232943]
[2025-05-07 17:26:50,058 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:50,058 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:50,059 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:50,061 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:26:50,061 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-05-07 17:26:50,094 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 22 statements into 1 equivalence classes.
[2025-05-07 17:26:50,117 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:26:50,117 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:50,117 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:50,118 INFO  L256         TraceCheckSpWp]: Trace formula consists of 302 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:50,119 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:50,130 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:26:50,130 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:26:50,268 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:26:50,268 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [530232943] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:26:50,268 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:26:50,268 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-05-07 17:26:50,268 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1662219619]
[2025-05-07 17:26:50,268 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:26:50,268 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:50,268 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:50,268 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:50,268 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:50,269 INFO  L87              Difference]: Start difference. First operand 4516 states and 85253 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:26:52,969 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:52,969 INFO  L93              Difference]: Finished difference Result 6371 states and 158524 transitions.
[2025-05-07 17:26:52,969 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:26:52,969 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 22
[2025-05-07 17:26:52,970 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:57,795 INFO  L225             Difference]: With dead ends: 6371
[2025-05-07 17:26:57,795 INFO  L226             Difference]: Without dead ends: 6371
[2025-05-07 17:26:57,795 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 51 GetRequests, 43 SyntacticMatches, 3 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:26:57,796 INFO  L437           NwaCegarLoop]: 409 mSDtfsCounter, 84 mSDsluCounter, 521 mSDsCounter, 0 mSdLazyCounter, 1257 mSolverCounterSat, 210 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 110 SdHoareTripleChecker+Valid, 930 SdHoareTripleChecker+Invalid, 1467 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 210 IncrementalHoareTripleChecker+Valid, 1257 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:57,796 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [110 Valid, 930 Invalid, 1467 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [210 Valid, 1257 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-05-07 17:26:57,798 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 6371 states.
[2025-05-07 17:27:09,736 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 6371 to 6371.
[2025-05-07 17:27:09,779 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 6371 states, 563 states have (on average 9.468916518650088) internal successors, (5331), 4688 states have internal predecessors, (5331), 5806 states have call successors, (5806), 281 states have call predecessors, (5806), 281 states have return successors, (147387), 1402 states have call predecessors, (147387), 5806 states have call successors, (147387)
[2025-05-07 17:27:10,941 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 6371 states to 6371 states and 158524 transitions.
[2025-05-07 17:27:10,941 INFO  L79                 Accepts]: Start accepts. Automaton has 6371 states and 158524 transitions. Word has length 22
[2025-05-07 17:27:10,941 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:10,941 INFO  L485      AbstractCegarLoop]: Abstraction has 6371 states and 158524 transitions.
[2025-05-07 17:27:10,942 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:27:10,942 INFO  L278                IsEmpty]: Start isEmpty. Operand 6371 states and 158524 transitions.
[2025-05-07 17:27:11,029 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 23
[2025-05-07 17:27:11,029 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:11,030 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:11,033 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-05-07 17:27:11,230 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable23
[2025-05-07 17:27:11,231 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:11,239 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:11,239 INFO  L85        PathProgramCache]: Analyzing trace with hash 600342933, now seen corresponding path program 2 times
[2025-05-07 17:27:11,240 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:11,240 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1932063751]
[2025-05-07 17:27:11,240 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:27:11,240 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:11,252 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 22 statements into 2 equivalence classes.
[2025-05-07 17:27:11,254 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:27:11,255 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:27:11,255 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:11,280 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:27:11,280 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:11,280 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1932063751]
[2025-05-07 17:27:11,280 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1932063751] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:27:11,280 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [484070129]
[2025-05-07 17:27:11,280 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:27:11,280 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:11,281 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:11,283 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:27:11,284 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-05-07 17:27:11,321 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 22 statements into 2 equivalence classes.
[2025-05-07 17:27:11,351 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:27:11,351 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:27:11,351 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:11,352 INFO  L256         TraceCheckSpWp]: Trace formula consists of 299 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:27:11,353 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:27:11,364 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:27:11,364 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:27:11,498 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:27:11,498 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [484070129] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:27:11,498 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:27:11,498 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-05-07 17:27:11,498 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1315817648]
[2025-05-07 17:27:11,498 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:27:11,498 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:11,499 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:11,499 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:11,499 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:11,499 INFO  L87              Difference]: Start difference. First operand 6371 states and 158524 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:27:16,029 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:16,029 INFO  L93              Difference]: Finished difference Result 7962 states and 259313 transitions.
[2025-05-07 17:27:16,030 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:27:16,030 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 22
[2025-05-07 17:27:16,030 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:27,133 INFO  L225             Difference]: With dead ends: 7962
[2025-05-07 17:27:27,133 INFO  L226             Difference]: Without dead ends: 7962
[2025-05-07 17:27:27,134 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 51 GetRequests, 43 SyntacticMatches, 3 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:27:27,134 INFO  L437           NwaCegarLoop]: 407 mSDtfsCounter, 83 mSDsluCounter, 753 mSDsCounter, 0 mSdLazyCounter, 1850 mSolverCounterSat, 226 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 122 SdHoareTripleChecker+Valid, 1160 SdHoareTripleChecker+Invalid, 2076 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 226 IncrementalHoareTripleChecker+Valid, 1850 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:27,134 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [122 Valid, 1160 Invalid, 2076 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [226 Valid, 1850 Invalid, 0 Unknown, 0 Unchecked, 1.8s Time]
[2025-05-07 17:27:27,137 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 7962 states.
[2025-05-07 17:27:50,177 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 7962 to 7962.
[2025-05-07 17:27:50,241 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 7962 states, 703 states have (on average 9.812233285917497) internal successors, (6898), 5859 states have internal predecessors, (6898), 7257 states have call successors, (7257), 351 states have call predecessors, (7257), 351 states have return successors, (245158), 1752 states have call predecessors, (245158), 7257 states have call successors, (245158)
[2025-05-07 17:27:52,599 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 7962 states to 7962 states and 259313 transitions.
[2025-05-07 17:27:52,599 INFO  L79                 Accepts]: Start accepts. Automaton has 7962 states and 259313 transitions. Word has length 22
[2025-05-07 17:27:52,599 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:52,599 INFO  L485      AbstractCegarLoop]: Abstraction has 7962 states and 259313 transitions.
[2025-05-07 17:27:52,599 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:27:52,599 INFO  L278                IsEmpty]: Start isEmpty. Operand 7962 states and 259313 transitions.
[2025-05-07 17:27:52,717 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-05-07 17:27:52,717 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:52,717 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:52,720 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-05-07 17:27:52,918 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable24,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:52,918 INFO  L403      AbstractCegarLoop]: === Iteration 25 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:52,927 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:52,928 INFO  L85        PathProgramCache]: Analyzing trace with hash 882689115, now seen corresponding path program 1 times
[2025-05-07 17:27:52,928 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:52,928 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1619249377]
[2025-05-07 17:27:52,928 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:52,929 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:52,940 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-05-07 17:27:52,948 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-05-07 17:27:52,948 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:52,948 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:52,964 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:27:52,964 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:52,964 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1619249377]
[2025-05-07 17:27:52,964 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1619249377] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:52,964 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:52,964 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:52,964 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [209906025]
[2025-05-07 17:27:52,964 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:52,964 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:52,965 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:52,965 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:52,965 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:52,965 INFO  L87              Difference]: Start difference. First operand 7962 states and 259313 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:27:59,822 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:59,823 INFO  L93              Difference]: Finished difference Result 10032 states and 578537 transitions.
[2025-05-07 17:27:59,823 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:59,823 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 23
[2025-05-07 17:27:59,824 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:28,972 INFO  L225             Difference]: With dead ends: 10032
[2025-05-07 17:28:28,972 INFO  L226             Difference]: Without dead ends: 10032
[2025-05-07 17:28:28,972 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-05-07 17:28:28,973 INFO  L437           NwaCegarLoop]: 241 mSDtfsCounter, 28 mSDsluCounter, 210 mSDsCounter, 0 mSdLazyCounter, 494 mSolverCounterSat, 100 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 58 SdHoareTripleChecker+Valid, 451 SdHoareTripleChecker+Invalid, 594 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 100 IncrementalHoareTripleChecker+Valid, 494 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:28,973 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [58 Valid, 451 Invalid, 594 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [100 Valid, 494 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:28:28,978 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 10032 states.
[2025-05-07 17:29:23,319 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 10032 to 9662.
[2025-05-07 17:29:23,456 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 9662 states, 1053 states have (on average 9.651471984805319) internal successors, (10163), 6509 states have internal predecessors, (10163), 8607 states have call successors, (8607), 526 states have call predecessors, (8607), 526 states have return successors, (442358), 2627 states have call predecessors, (442358), 8607 states have call successors, (442358)
[2025-05-07 17:29:28,701 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 9662 states to 9662 states and 461128 transitions.
[2025-05-07 17:29:28,701 INFO  L79                 Accepts]: Start accepts. Automaton has 9662 states and 461128 transitions. Word has length 23
[2025-05-07 17:29:28,701 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:29:28,701 INFO  L485      AbstractCegarLoop]: Abstraction has 9662 states and 461128 transitions.
[2025-05-07 17:29:28,701 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:29:28,701 INFO  L278                IsEmpty]: Start isEmpty. Operand 9662 states and 461128 transitions.
[2025-05-07 17:29:28,933 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-05-07 17:29:28,933 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:29:28,934 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:29:28,934 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable25
[2025-05-07 17:29:28,934 INFO  L403      AbstractCegarLoop]: === Iteration 26 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:29:28,935 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:29:28,935 INFO  L85        PathProgramCache]: Analyzing trace with hash 1603287286, now seen corresponding path program 1 times
[2025-05-07 17:29:28,935 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:29:28,935 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1452528815]
[2025-05-07 17:29:28,935 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:29:28,935 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:29:28,938 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-05-07 17:29:28,940 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-05-07 17:29:28,940 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:29:28,940 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:29:28,953 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:29:28,954 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:29:28,954 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1452528815]
[2025-05-07 17:29:28,954 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1452528815] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:29:28,954 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:29:28,954 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:29:28,954 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [939890556]
[2025-05-07 17:29:28,954 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:29:28,954 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:29:28,954 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:29:28,954 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:29:28,954 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:29:28,954 INFO  L87              Difference]: Start difference. First operand 9662 states and 461128 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:29:42,030 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:42,030 INFO  L93              Difference]: Finished difference Result 12082 states and 982119 transitions.
[2025-05-07 17:29:42,031 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:29:42,031 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 23
[2025-05-07 17:29:42,031 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:30:42,161 INFO  L225             Difference]: With dead ends: 12082
[2025-05-07 17:30:42,161 INFO  L226             Difference]: Without dead ends: 12082
[2025-05-07 17:30:42,162 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-05-07 17:30:42,162 INFO  L437           NwaCegarLoop]: 241 mSDtfsCounter, 28 mSDsluCounter, 193 mSDsCounter, 0 mSdLazyCounter, 578 mSolverCounterSat, 102 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 71 SdHoareTripleChecker+Valid, 434 SdHoareTripleChecker+Invalid, 680 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 102 IncrementalHoareTripleChecker+Valid, 578 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-05-07 17:30:42,162 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [71 Valid, 434 Invalid, 680 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [102 Valid, 578 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-05-07 17:30:42,165 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 12082 states.
[2025-05-07 17:32:17,032 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 12082 to 11362.
[2025-05-07 17:32:17,369 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 11362 states, 1403 states have (on average 10.568781183178903) internal successors, (14828), 7159 states have internal predecessors, (14828), 9957 states have call successors, (9957), 701 states have call predecessors, (9957), 701 states have return successors, (690240), 3502 states have call predecessors, (690240), 9957 states have call successors, (690240)
[2025-05-07 17:32:27,213 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 11362 states to 11362 states and 715025 transitions.
[2025-05-07 17:32:27,214 INFO  L79                 Accepts]: Start accepts. Automaton has 11362 states and 715025 transitions. Word has length 23
[2025-05-07 17:32:27,214 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:32:27,214 INFO  L485      AbstractCegarLoop]: Abstraction has 11362 states and 715025 transitions.
[2025-05-07 17:32:27,214 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:32:27,214 INFO  L278                IsEmpty]: Start isEmpty. Operand 11362 states and 715025 transitions.
[2025-05-07 17:32:27,795 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-05-07 17:32:27,795 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:32:27,796 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:32:27,796 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable26
[2025-05-07 17:32:27,796 INFO  L403      AbstractCegarLoop]: === Iteration 27 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:32:27,799 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:32:27,799 INFO  L85        PathProgramCache]: Analyzing trace with hash -1250483668, now seen corresponding path program 1 times
[2025-05-07 17:32:27,799 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:32:27,799 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [322004598]
[2025-05-07 17:32:27,799 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:32:27,799 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:32:27,826 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-05-07 17:32:27,846 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-05-07 17:32:27,846 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:32:27,846 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:32:27,933 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:32:27,933 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:32:27,933 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [322004598]
[2025-05-07 17:32:27,933 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [322004598] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:32:27,933 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:32:27,933 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:32:27,933 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1044768056]
[2025-05-07 17:32:27,933 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:32:27,934 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:32:27,934 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:32:27,935 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:32:27,935 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:32:27,935 INFO  L87              Difference]: Start difference. First operand 11362 states and 715025 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:32:51,686 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:32:51,686 INFO  L93              Difference]: Finished difference Result 14812 states and 1640835 transitions.
[2025-05-07 17:32:51,687 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:32:51,687 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 23
[2025-05-07 17:32:51,687 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:34:27,670 INFO  L225             Difference]: With dead ends: 14812
[2025-05-07 17:34:27,671 INFO  L226             Difference]: Without dead ends: 14812
[2025-05-07 17:34:27,671 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-05-07 17:34:27,672 INFO  L437           NwaCegarLoop]: 244 mSDtfsCounter, 28 mSDsluCounter, 218 mSDsCounter, 0 mSdLazyCounter, 245 mSolverCounterSat, 211 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 103 SdHoareTripleChecker+Valid, 462 SdHoareTripleChecker+Invalid, 456 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 211 IncrementalHoareTripleChecker+Valid, 245 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:34:27,672 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [103 Valid, 462 Invalid, 456 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [211 Valid, 245 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:34:27,682 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 14812 states.
[2025-05-07 17:37:20,437 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 14812 to 13062.
[2025-05-07 17:37:20,814 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 13062 states, 1753 states have (on average 9.525385054192812) internal successors, (16698), 7809 states have internal predecessors, (16698), 11307 states have call successors, (11307), 876 states have call predecessors, (11307), 876 states have return successors, (805978), 4377 states have call predecessors, (805978), 11307 states have call successors, (805978)
[2025-05-07 17:37:32,210 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 13062 states to 13062 states and 833983 transitions.
[2025-05-07 17:37:32,210 INFO  L79                 Accepts]: Start accepts. Automaton has 13062 states and 833983 transitions. Word has length 23
[2025-05-07 17:37:32,210 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:37:32,210 INFO  L485      AbstractCegarLoop]: Abstraction has 13062 states and 833983 transitions.
[2025-05-07 17:37:32,210 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:37:32,210 INFO  L278                IsEmpty]: Start isEmpty. Operand 13062 states and 833983 transitions.
[2025-05-07 17:37:32,535 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-05-07 17:37:32,535 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:37:32,535 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:37:32,535 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable27
[2025-05-07 17:37:32,535 INFO  L403      AbstractCegarLoop]: === Iteration 28 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:37:32,536 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:37:32,537 INFO  L85        PathProgramCache]: Analyzing trace with hash -644372417, now seen corresponding path program 1 times
[2025-05-07 17:37:32,537 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:37:32,537 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [961036552]
[2025-05-07 17:37:32,537 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:37:32,537 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:37:32,547 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-05-07 17:37:32,557 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-05-07 17:37:32,557 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:37:32,557 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:37:32,603 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:37:32,603 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:37:32,603 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [961036552]
[2025-05-07 17:37:32,603 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [961036552] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:37:32,603 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:37:32,603 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:37:32,603 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1481650237]
[2025-05-07 17:37:32,604 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:37:32,604 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:37:32,604 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:37:32,604 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:37:32,604 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:37:32,605 INFO  L87              Difference]: Start difference. First operand 13062 states and 833983 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:37:55,686 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:37:55,686 INFO  L93              Difference]: Finished difference Result 15502 states and 1481049 transitions.
[2025-05-07 17:37:55,687 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:37:55,687 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 23
[2025-05-07 17:37:55,688 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:39:37,556 INFO  L225             Difference]: With dead ends: 15502
[2025-05-07 17:39:37,556 INFO  L226             Difference]: Without dead ends: 15502
[2025-05-07 17:39:37,556 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-05-07 17:39:37,557 INFO  L437           NwaCegarLoop]: 226 mSDtfsCounter, 28 mSDsluCounter, 173 mSDsCounter, 0 mSdLazyCounter, 580 mSolverCounterSat, 102 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 73 SdHoareTripleChecker+Valid, 399 SdHoareTripleChecker+Invalid, 682 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 102 IncrementalHoareTripleChecker+Valid, 580 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:39:37,557 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [73 Valid, 399 Invalid, 682 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [102 Valid, 580 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:39:37,561 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15502 states.
[2025-05-07 17:41:51,672 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15502 to 14762.
[2025-05-07 17:41:52,008 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 14762 states, 2103 states have (on average 10.241559676652402) internal successors, (21538), 8459 states have internal predecessors, (21538), 12657 states have call successors, (12657), 1051 states have call predecessors, (12657), 1051 states have return successors, (1104542), 5252 states have call predecessors, (1104542), 12657 states have call successors, (1104542)
[2025-05-07 17:42:09,197 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 14762 states to 14762 states and 1138737 transitions.
[2025-05-07 17:42:09,197 INFO  L79                 Accepts]: Start accepts. Automaton has 14762 states and 1138737 transitions. Word has length 23
[2025-05-07 17:42:09,197 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:42:09,197 INFO  L485      AbstractCegarLoop]: Abstraction has 14762 states and 1138737 transitions.
[2025-05-07 17:42:09,198 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, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:42:09,198 INFO  L278                IsEmpty]: Start isEmpty. Operand 14762 states and 1138737 transitions.
[2025-05-07 17:42:09,595 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-05-07 17:42:09,595 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:42:09,595 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:42:09,595 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable28
[2025-05-07 17:42:09,595 INFO  L403      AbstractCegarLoop]: === Iteration 29 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:42:09,596 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:42:09,596 INFO  L85        PathProgramCache]: Analyzing trace with hash 1546043826, now seen corresponding path program 1 times
[2025-05-07 17:42:09,596 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:42:09,597 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1802707770]
[2025-05-07 17:42:09,597 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:42:09,597 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:42:09,607 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-05-07 17:42:09,612 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-05-07 17:42:09,612 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:42:09,612 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:42:09,638 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 8 proven. 0 refuted. 0 times theorem prover too weak. 22 trivial. 0 not checked.
[2025-05-07 17:42:09,638 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:42:09,638 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1802707770]
[2025-05-07 17:42:09,638 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1802707770] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:42:09,638 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:42:09,638 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:42:09,638 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [807124657]
[2025-05-07 17:42:09,639 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:42:09,639 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:42:09,639 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:42:09,639 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:42:09,639 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:42:09,639 INFO  L87              Difference]: Start difference. First operand 14762 states and 1138737 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, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-05-07 17:42:33,997 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:42:33,998 INFO  L93              Difference]: Finished difference Result 15842 states and 1576711 transitions.
[2025-05-07 17:42:33,999 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:42:33,999 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, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5) Word has length 23
[2025-05-07 17:42:33,999 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:44:19,044 INFO  L225             Difference]: With dead ends: 15842
[2025-05-07 17:44:19,044 INFO  L226             Difference]: Without dead ends: 15842
[2025-05-07 17:44:19,044 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-05-07 17:44:19,044 INFO  L437           NwaCegarLoop]: 244 mSDtfsCounter, 28 mSDsluCounter, 250 mSDsCounter, 0 mSdLazyCounter, 480 mSolverCounterSat, 72 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 43 SdHoareTripleChecker+Valid, 494 SdHoareTripleChecker+Invalid, 552 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 72 IncrementalHoareTripleChecker+Valid, 480 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:44:19,045 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [43 Valid, 494 Invalid, 552 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [72 Valid, 480 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:44:19,049 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15842 states.
[2025-05-07 17:46:46,476 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15842 to 14762.
[2025-05-07 17:46:46,820 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 14762 states, 2103 states have (on average 10.241559676652402) internal successors, (21538), 8459 states have internal predecessors, (21538), 12657 states have call successors, (12657), 1051 states have call predecessors, (12657), 1051 states have return successors, (1100438), 5252 states have call predecessors, (1100438), 12657 states have call successors, (1100438)
[2025-05-07 17:47:04,136 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 14762 states to 14762 states and 1134633 transitions.
[2025-05-07 17:47:04,136 INFO  L79                 Accepts]: Start accepts. Automaton has 14762 states and 1134633 transitions. Word has length 23
[2025-05-07 17:47:04,136 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:47:04,136 INFO  L485      AbstractCegarLoop]: Abstraction has 14762 states and 1134633 transitions.
[2025-05-07 17:47:04,136 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, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-05-07 17:47:04,136 INFO  L278                IsEmpty]: Start isEmpty. Operand 14762 states and 1134633 transitions.
[2025-05-07 17:47:04,731 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 27
[2025-05-07 17:47:04,731 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:47:04,731 INFO  L218           NwaCegarLoop]: trace histogram [6, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:47:04,732 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable29
[2025-05-07 17:47:04,732 INFO  L403      AbstractCegarLoop]: === Iteration 30 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:47:04,732 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:47:04,732 INFO  L85        PathProgramCache]: Analyzing trace with hash -131117558, now seen corresponding path program 1 times
[2025-05-07 17:47:04,732 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:47:04,732 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1701347477]
[2025-05-07 17:47:04,732 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:47:04,733 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:47:04,740 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-05-07 17:47:04,746 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-05-07 17:47:04,746 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:47:04,746 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:47:04,797 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 22 proven. 4 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-05-07 17:47:04,797 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:47:04,797 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1701347477]
[2025-05-07 17:47:04,797 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1701347477] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:47:04,797 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1775209189]
[2025-05-07 17:47:04,797 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:47:04,797 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:47:04,800 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:47:04,802 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:47:04,803 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-05-07 17:47:04,845 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 26 statements into 1 equivalence classes.
[2025-05-07 17:47:04,879 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 26 of 26 statements.
[2025-05-07 17:47:04,879 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:47:04,879 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:47:04,881 INFO  L256         TraceCheckSpWp]: Trace formula consists of 358 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:47:04,883 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:47:04,903 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 22 proven. 4 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-05-07 17:47:04,903 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:47:05,121 INFO  L134       CoverageAnalysis]: Checked inductivity of 45 backedges. 22 proven. 4 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-05-07 17:47:05,121 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1775209189] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:47:05,121 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:47:05,121 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-05-07 17:47:05,121 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1160412268]
[2025-05-07 17:47:05,121 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:47:05,121 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:47:05,121 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:47:05,122 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:47:05,122 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:47:05,122 INFO  L87              Difference]: Start difference. First operand 14762 states and 1134633 transitions. Second operand  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (8), 4 states have call predecessors, (8), 4 states have call successors, (8)
