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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:27,343 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:27,449 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_614936c0-2689-4965-b21d-986d3b67525f/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:27,460 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:27,461 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:27,495 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:27,496 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:27,496 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:27,497 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:27,497 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:27,497 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:27,498 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:27,498 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:27,498 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:27,498 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:27,498 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:27,498 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:27,499 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:27,499 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:27,499 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:27,499 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:27,499 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:27,499 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:27,499 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:27,500 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:27,501 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:27,501 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:27,852 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:27,864 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:27,867 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:27,870 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:27,871 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:27,872 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_614936c0-2689-4965-b21d-986d3b67525f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-079.smt2
[2025-04-28 21:21:27,873 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:27,880 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:28,018 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_614936c0-2689-4965-b21d-986d3b67525f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-079.smt2
[2025-04-28 21:21:28,024 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:28,027 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:28,028 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:28,028 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:28,028 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:28,035 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,055 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28 Unit
[2025-04-28 21:21:28,055 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:28,056 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:28,056 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:28,056 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:28,073 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,073 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,093 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,093 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,095 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,095 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,097 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,098 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,098 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,113 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:28,114 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:28,114 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:28,114 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:28,115 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (1/1) ...
[2025-04-28 21:21:28,118 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:28,136 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,155 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:28,159 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,178 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:28,178 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:28,178 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:28,178 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:28,178 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:28,179 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:28,179 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:28,180 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:28,180 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:28,226 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:28,229 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:28,291 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:28,292 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:28,309 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:28,310 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:28,311 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:28 BoogieIcfgContainer
[2025-04-28 21:21:28,311 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:28,316 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:28,316 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:28,321 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:28,321 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:28" (1/3) ...
[2025-04-28 21:21:28,322 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@28cd0389 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:28, skipping insertion in model container
[2025-04-28 21:21:28,322 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:28" (2/3) ...
[2025-04-28 21:21:28,324 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@28cd0389 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:28, skipping insertion in model container
[2025-04-28 21:21:28,324 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:28" (3/3) ...
[2025-04-28 21:21:28,326 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:28,343 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:28,345 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 13 locations, 17 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:28,395 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:28,409 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;@10a52f7d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:28,409 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:28,414 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 13 states, 6 states have (on average 1.3333333333333333) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 2 states have return successors, (3), 3 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:28,421 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:28,421 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,422 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,423 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,428 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,429 INFO  L85        PathProgramCache]: Analyzing trace with hash -1672547219, now seen corresponding path program 1 times
[2025-04-28 21:21:28,437 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,438 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [808998701]
[2025-04-28 21:21:28,438 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,439 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,465 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:28,482 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:28,483 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,483 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,622 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:28,622 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,624 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [808998701]
[2025-04-28 21:21:28,625 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [808998701] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,625 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,629 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:28,631 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1963576673]
[2025-04-28 21:21:28,631 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,637 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:28,638 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,673 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:28,675 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,677 INFO  L87              Difference]: Start difference. First operand  has 13 states, 6 states have (on average 1.3333333333333333) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 2 states have return successors, (3), 3 states have call predecessors, (3), 3 states have call successors, (3) Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:28,723 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,724 INFO  L93              Difference]: Finished difference Result 13 states and 14 transitions.
[2025-04-28 21:21:28,726 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:28,729 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:28,730 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,738 INFO  L225             Difference]: With dead ends: 13
[2025-04-28 21:21:28,739 INFO  L226             Difference]: Without dead ends: 13
[2025-04-28 21:21:28,742 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,746 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 1 mSDsluCounter, 15 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 26 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,748 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 26 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:28,764 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 13 states.
[2025-04-28 21:21:28,789 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 13 to 13.
[2025-04-28 21:21:28,790 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 13 states, 6 states have (on average 1.1666666666666667) internal successors, (7), 7 states have internal predecessors, (7), 3 states have call successors, (3), 2 states have call predecessors, (3), 3 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:28,794 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 13 states to 13 states and 14 transitions.
[2025-04-28 21:21:28,795 INFO  L79                 Accepts]: Start accepts. Automaton has 13 states and 14 transitions. Word has length 9
[2025-04-28 21:21:28,795 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,796 INFO  L485      AbstractCegarLoop]: Abstraction has 13 states and 14 transitions.
[2025-04-28 21:21:28,796 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:28,797 INFO  L278                IsEmpty]: Start isEmpty. Operand 13 states and 14 transitions.
[2025-04-28 21:21:28,798 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:28,798 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,798 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,799 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:28,799 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,800 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,800 INFO  L85        PathProgramCache]: Analyzing trace with hash 13498287, now seen corresponding path program 1 times
[2025-04-28 21:21:28,800 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,800 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [270546575]
[2025-04-28 21:21:28,800 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,800 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,806 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:28,821 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:28,821 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,821 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,947 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:28,948 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,948 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [270546575]
[2025-04-28 21:21:28,948 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [270546575] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,948 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1168015991]
[2025-04-28 21:21:28,948 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,949 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,951 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,954 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:28,957 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,993 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:29,005 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:29,005 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,005 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,008 INFO  L256         TraceCheckSpWp]: Trace formula consists of 36 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,013 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,142 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:29,143 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:29,490 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:29,491 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1168015991] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:29,491 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:29,491 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:29,492 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2026867820]
[2025-04-28 21:21:29,492 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,493 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:29,493 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,494 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:29,494 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=38, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,494 INFO  L87              Difference]: Start difference. First operand 13 states and 14 transitions. Second operand  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:29,559 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,559 INFO  L93              Difference]: Finished difference Result 15 states and 16 transitions.
[2025-04-28 21:21:29,560 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:29,560 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5) Word has length 13
[2025-04-28 21:21:29,561 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,561 INFO  L225             Difference]: With dead ends: 15
[2025-04-28 21:21:29,561 INFO  L226             Difference]: Without dead ends: 15
[2025-04-28 21:21:29,561 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 23 SyntacticMatches, 2 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=49, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:29,563 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 5 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 16 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 32 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 16 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,566 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 32 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 16 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:29,566 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15 states.
[2025-04-28 21:21:29,571 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15 to 15.
[2025-04-28 21:21:29,571 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 15 states, 7 states have (on average 1.1428571428571428) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:29,572 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 15 states to 15 states and 16 transitions.
[2025-04-28 21:21:29,572 INFO  L79                 Accepts]: Start accepts. Automaton has 15 states and 16 transitions. Word has length 13
[2025-04-28 21:21:29,573 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,573 INFO  L485      AbstractCegarLoop]: Abstraction has 15 states and 16 transitions.
[2025-04-28 21:21:29,574 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:29,574 INFO  L278                IsEmpty]: Start isEmpty. Operand 15 states and 16 transitions.
[2025-04-28 21:21:29,574 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:29,575 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,575 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:29,581 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:29,775 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,776 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,776 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,776 INFO  L85        PathProgramCache]: Analyzing trace with hash -1177266959, now seen corresponding path program 2 times
[2025-04-28 21:21:29,777 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,777 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [936564161]
[2025-04-28 21:21:29,777 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:29,777 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,786 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:29,798 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:29,798 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:29,798 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,021 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:30,021 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,021 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [936564161]
[2025-04-28 21:21:30,022 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [936564161] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,022 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1981897795]
[2025-04-28 21:21:30,022 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:30,022 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,025 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,027 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:30,031 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:30,065 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:30,079 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:30,079 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:30,079 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,081 INFO  L256         TraceCheckSpWp]: Trace formula consists of 48 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:30,083 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,130 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:30,131 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:30,595 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:30,595 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1981897795] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:30,595 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:30,595 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 10
[2025-04-28 21:21:30,595 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1266171347]
[2025-04-28 21:21:30,595 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,596 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:30,596 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,597 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:30,597 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:30,597 INFO  L87              Difference]: Start difference. First operand 15 states and 16 transitions. Second operand  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:30,660 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,661 INFO  L93              Difference]: Finished difference Result 17 states and 18 transitions.
[2025-04-28 21:21:30,661 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:30,661 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 17
[2025-04-28 21:21:30,662 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,662 INFO  L225             Difference]: With dead ends: 17
[2025-04-28 21:21:30,662 INFO  L226             Difference]: Without dead ends: 17
[2025-04-28 21:21:30,662 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 43 GetRequests, 30 SyntacticMatches, 3 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=42, Invalid=90, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:30,663 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 8 mSDsluCounter, 22 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 33 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,664 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 33 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:30,664 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17 states.
[2025-04-28 21:21:30,667 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 17 to 17.
[2025-04-28 21:21:30,667 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 17 states, 8 states have (on average 1.125) internal successors, (9), 9 states have internal predecessors, (9), 3 states have call successors, (3), 2 states have call predecessors, (3), 5 states have return successors, (6), 5 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:30,668 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 18 transitions.
[2025-04-28 21:21:30,668 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 18 transitions. Word has length 17
[2025-04-28 21:21:30,668 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,668 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 18 transitions.
[2025-04-28 21:21:30,668 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:30,668 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 18 transitions.
[2025-04-28 21:21:30,669 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:30,669 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,669 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,675 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:30,873 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,873 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,874 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,874 INFO  L85        PathProgramCache]: Analyzing trace with hash 329141299, now seen corresponding path program 3 times
[2025-04-28 21:21:30,874 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,874 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2003797517]
[2025-04-28 21:21:30,874 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:30,874 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,881 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:30,909 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:30,912 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:30,912 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,377 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 1 proven. 14 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:31,378 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,378 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2003797517]
[2025-04-28 21:21:31,378 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2003797517] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,378 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1583533277]
[2025-04-28 21:21:31,378 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:31,378 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,381 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,383 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:31,387 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,418 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:31,433 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:31,433 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:31,433 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,434 INFO  L256         TraceCheckSpWp]: Trace formula consists of 60 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,436 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,609 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 12 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:31,609 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:32,461 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 15 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:32,463 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1583533277] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:32,463 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:32,463 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 8, 10] total 20
[2025-04-28 21:21:32,463 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1612998335]
[2025-04-28 21:21:32,463 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,464 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:32,464 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,466 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:32,467 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=69, Invalid=311, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:32,468 INFO  L87              Difference]: Start difference. First operand 17 states and 18 transitions. Second operand  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (13), 7 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:21:32,883 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,884 INFO  L93              Difference]: Finished difference Result 21 states and 22 transitions.
[2025-04-28 21:21:32,885 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:32,885 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (13), 7 states have call predecessors, (13), 11 states have call successors, (13) Word has length 21
[2025-04-28 21:21:32,885 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,886 INFO  L225             Difference]: With dead ends: 21
[2025-04-28 21:21:32,886 INFO  L226             Difference]: Without dead ends: 21
[2025-04-28 21:21:32,887 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 57 GetRequests, 29 SyntacticMatches, 4 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 136 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=150, Invalid=500, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:32,887 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 25 mSDsluCounter, 64 mSDsCounter, 0 mSdLazyCounter, 51 mSolverCounterSat, 30 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 75 SdHoareTripleChecker+Invalid, 81 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 30 IncrementalHoareTripleChecker+Valid, 51 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,888 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 75 Invalid, 81 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [30 Valid, 51 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:32,889 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 21 states.
[2025-04-28 21:21:32,892 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 21 to 21.
[2025-04-28 21:21:32,892 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 21 states, 10 states have (on average 1.1) internal successors, (11), 11 states have internal predecessors, (11), 3 states have call successors, (3), 2 states have call predecessors, (3), 7 states have return successors, (8), 7 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:32,893 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 21 states to 21 states and 22 transitions.
[2025-04-28 21:21:32,893 INFO  L79                 Accepts]: Start accepts. Automaton has 21 states and 22 transitions. Word has length 21
[2025-04-28 21:21:32,893 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,893 INFO  L485      AbstractCegarLoop]: Abstraction has 21 states and 22 transitions.
[2025-04-28 21:21:32,894 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (13), 7 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:21:32,894 INFO  L278                IsEmpty]: Start isEmpty. Operand 21 states and 22 transitions.
[2025-04-28 21:21:32,894 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:32,895 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,895 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,899 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:33,095 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,095 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,096 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,096 INFO  L85        PathProgramCache]: Analyzing trace with hash 1866336439, now seen corresponding path program 4 times
[2025-04-28 21:21:33,096 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,096 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1959554259]
[2025-04-28 21:21:33,096 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:33,096 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,104 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:33,137 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:33,137 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:33,138 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,375 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 34 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:21:33,375 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,375 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1959554259]
[2025-04-28 21:21:33,376 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1959554259] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,376 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [763493018]
[2025-04-28 21:21:33,376 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:33,376 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,379 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,381 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:33,386 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,425 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:33,444 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:33,444 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:33,444 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,445 INFO  L256         TraceCheckSpWp]: Trace formula consists of 84 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,446 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,529 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 30 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:33,529 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:35,295 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 40 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:35,295 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [763493018] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:35,296 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:35,296 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 10, 14] total 19
[2025-04-28 21:21:35,296 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1569939580]
[2025-04-28 21:21:35,296 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,296 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:35,296 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,297 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:35,297 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=89, Invalid=253, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:35,298 INFO  L87              Difference]: Start difference. First operand 21 states and 22 transitions. Second operand  has 19 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 18 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (15), 7 states have call predecessors, (15), 11 states have call successors, (15)
[2025-04-28 21:21:35,500 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,500 INFO  L93              Difference]: Finished difference Result 25 states and 26 transitions.
[2025-04-28 21:21:35,501 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:35,501 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 18 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (15), 7 states have call predecessors, (15), 11 states have call successors, (15) Word has length 29
[2025-04-28 21:21:35,501 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,502 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:21:35,502 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:21:35,503 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 78 GetRequests, 48 SyntacticMatches, 6 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 125 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=194, Invalid=456, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:35,503 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 17 mSDsluCounter, 62 mSDsCounter, 0 mSdLazyCounter, 45 mSolverCounterSat, 19 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 73 SdHoareTripleChecker+Invalid, 64 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 19 IncrementalHoareTripleChecker+Valid, 45 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,504 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 73 Invalid, 64 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [19 Valid, 45 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:35,504 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:21:35,507 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 25.
[2025-04-28 21:21:35,508 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 25 states, 12 states have (on average 1.0833333333333333) internal successors, (13), 13 states have internal predecessors, (13), 3 states have call successors, (3), 2 states have call predecessors, (3), 9 states have return successors, (10), 9 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:35,508 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 26 transitions.
[2025-04-28 21:21:35,509 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 26 transitions. Word has length 29
[2025-04-28 21:21:35,509 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,509 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 26 transitions.
[2025-04-28 21:21:35,509 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 18 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (15), 7 states have call predecessors, (15), 11 states have call successors, (15)
[2025-04-28 21:21:35,509 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 26 transitions.
[2025-04-28 21:21:35,510 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:35,510 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,510 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,516 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:35,715 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:21:35,715 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,716 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,716 INFO  L85        PathProgramCache]: Analyzing trace with hash -254857925, now seen corresponding path program 5 times
[2025-04-28 21:21:35,716 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,716 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [107177078]
[2025-04-28 21:21:35,716 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:35,716 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,722 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 37 statements into 8 equivalence classes.
[2025-04-28 21:21:35,761 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:35,761 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s)
[2025-04-28 21:21:35,761 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,254 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 68 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:36,255 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,255 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [107177078]
[2025-04-28 21:21:36,255 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [107177078] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,255 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2083219910]
[2025-04-28 21:21:36,255 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:36,255 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,258 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,260 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:36,265 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,316 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 37 statements into 8 equivalence classes.
[2025-04-28 21:21:36,343 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:36,343 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s)
[2025-04-28 21:21:36,343 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,344 INFO  L256         TraceCheckSpWp]: Trace formula consists of 108 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,346 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,591 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 56 refuted. 0 times theorem prover too weak. 49 trivial. 0 not checked.
[2025-04-28 21:21:36,591 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,066 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 77 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:21:40,066 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2083219910] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,066 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,066 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 12, 18] total 31
[2025-04-28 21:21:40,066 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1889173006]
[2025-04-28 21:21:40,066 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,067 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 31 states
[2025-04-28 21:21:40,067 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,068 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 31 interpolants.
[2025-04-28 21:21:40,068 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=159, Invalid=771, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:21:40,069 INFO  L87              Difference]: Start difference. First operand 25 states and 26 transitions. Second operand  has 31 states, 18 states have (on average 1.8333333333333333) internal successors, (33), 30 states have internal predecessors, (33), 14 states have call successors, (14), 1 states have call predecessors, (14), 17 states have return successors, (25), 15 states have call predecessors, (25), 14 states have call successors, (25)
[2025-04-28 21:21:40,511 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,511 INFO  L93              Difference]: Finished difference Result 27 states and 28 transitions.
[2025-04-28 21:21:40,511 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:40,512 INFO  L79                 Accepts]: Start accepts. Automaton has  has 31 states, 18 states have (on average 1.8333333333333333) internal successors, (33), 30 states have internal predecessors, (33), 14 states have call successors, (14), 1 states have call predecessors, (14), 17 states have return successors, (25), 15 states have call predecessors, (25), 14 states have call successors, (25) Word has length 37
[2025-04-28 21:21:40,512 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,513 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:40,513 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:40,514 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 101 GetRequests, 54 SyntacticMatches, 8 SemanticMatches, 39 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 396 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=369, Invalid=1271, Unknown=0, NotChecked=0, Total=1640
[2025-04-28 21:21:40,514 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 39 mSDsluCounter, 112 mSDsCounter, 0 mSdLazyCounter, 78 mSolverCounterSat, 44 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 39 SdHoareTripleChecker+Valid, 123 SdHoareTripleChecker+Invalid, 122 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 44 IncrementalHoareTripleChecker+Valid, 78 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,515 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [39 Valid, 123 Invalid, 122 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [44 Valid, 78 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:40,515 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:40,519 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:40,519 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 3 states have call successors, (3), 2 states have call predecessors, (3), 10 states have return successors, (11), 10 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:40,521 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 28 transitions.
[2025-04-28 21:21:40,523 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 28 transitions. Word has length 37
[2025-04-28 21:21:40,523 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,523 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 28 transitions.
[2025-04-28 21:21:40,524 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 31 states, 18 states have (on average 1.8333333333333333) internal successors, (33), 30 states have internal predecessors, (33), 14 states have call successors, (14), 1 states have call predecessors, (14), 17 states have return successors, (25), 15 states have call predecessors, (25), 14 states have call successors, (25)
[2025-04-28 21:21:40,524 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 28 transitions.
[2025-04-28 21:21:40,525 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:40,527 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,527 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,533 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:40,731 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,731 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,732 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,732 INFO  L85        PathProgramCache]: Analyzing trace with hash 1201858173, now seen corresponding path program 6 times
[2025-04-28 21:21:40,732 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,732 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [575227553]
[2025-04-28 21:21:40,732 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:40,732 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,745 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 41 statements into 9 equivalence classes.
[2025-04-28 21:21:40,766 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 9 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:40,766 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 9 check-sat command(s)
[2025-04-28 21:21:40,766 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,080 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 4 proven. 75 refuted. 0 times theorem prover too weak. 57 trivial. 0 not checked.
[2025-04-28 21:21:41,080 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,080 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [575227553]
[2025-04-28 21:21:41,080 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [575227553] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,080 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [843289943]
[2025-04-28 21:21:41,081 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:41,081 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,083 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,085 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:41,089 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,181 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 41 statements into 9 equivalence classes.
[2025-04-28 21:21:41,213 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 9 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:41,213 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 9 check-sat command(s)
[2025-04-28 21:21:41,213 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,214 INFO  L256         TraceCheckSpWp]: Trace formula consists of 120 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,216 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,276 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 64 trivial. 0 not checked.
[2025-04-28 21:21:41,277 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,380 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 100 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:45,380 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [843289943] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,380 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,380 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 13, 20] total 23
[2025-04-28 21:21:45,381 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1859025243]
[2025-04-28 21:21:45,381 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,381 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:45,381 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,382 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:45,382 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=141, Invalid=365, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:45,383 INFO  L87              Difference]: Start difference. First operand 27 states and 28 transitions. Second operand  has 23 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 22 states have internal predecessors, (24), 13 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 13 states have call successors, (20)
[2025-04-28 21:21:45,564 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,564 INFO  L93              Difference]: Finished difference Result 29 states and 30 transitions.
[2025-04-28 21:21:45,564 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:45,564 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 22 states have internal predecessors, (24), 13 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 13 states have call successors, (20) Word has length 41
[2025-04-28 21:21:45,565 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,565 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:45,566 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:21:45,566 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 109 GetRequests, 71 SyntacticMatches, 9 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 245 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=301, Invalid=629, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:21:45,567 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 47 mSDsluCounter, 64 mSDsCounter, 0 mSdLazyCounter, 49 mSolverCounterSat, 45 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 58 SdHoareTripleChecker+Valid, 75 SdHoareTripleChecker+Invalid, 94 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 45 IncrementalHoareTripleChecker+Valid, 49 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,567 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [58 Valid, 75 Invalid, 94 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [45 Valid, 49 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,568 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:21:45,571 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:21:45,571 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 14 states have (on average 1.0714285714285714) internal successors, (15), 15 states have internal predecessors, (15), 3 states have call successors, (3), 2 states have call predecessors, (3), 11 states have return successors, (12), 11 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:45,572 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 30 transitions.
[2025-04-28 21:21:45,572 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 30 transitions. Word has length 41
[2025-04-28 21:21:45,573 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,573 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 30 transitions.
[2025-04-28 21:21:45,573 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 22 states have internal predecessors, (24), 13 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 13 states have call successors, (20)
[2025-04-28 21:21:45,573 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 30 transitions.
[2025-04-28 21:21:45,574 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:21:45,574 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,574 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,579 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:45,778 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,778 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,778 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,778 INFO  L85        PathProgramCache]: Analyzing trace with hash -1636582977, now seen corresponding path program 7 times
[2025-04-28 21:21:45,779 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,779 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1465525417]
[2025-04-28 21:21:45,779 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:45,779 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,783 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:45,797 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:45,797 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,797 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,067 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:21:46,067 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,067 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1465525417]
[2025-04-28 21:21:46,067 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1465525417] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,067 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2120247843]
[2025-04-28 21:21:46,068 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:46,068 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,070 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,072 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:46,076 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,214 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 45 statements into 1 equivalence classes.
[2025-04-28 21:21:46,233 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:46,233 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,233 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,234 INFO  L256         TraceCheckSpWp]: Trace formula consists of 132 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,236 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,310 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:21:46,310 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,717 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 126 refuted. 0 times theorem prover too weak. 45 trivial. 0 not checked.
[2025-04-28 21:21:51,717 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2120247843] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,718 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,718 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 22] total 24
[2025-04-28 21:21:51,718 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [710368351]
[2025-04-28 21:21:51,718 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,718 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:51,718 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,719 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:51,719 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=154, Invalid=398, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:51,720 INFO  L87              Difference]: Start difference. First operand 29 states and 30 transitions. Second operand  has 24 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 13 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:21:51,882 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,882 INFO  L93              Difference]: Finished difference Result 31 states and 32 transitions.
[2025-04-28 21:21:51,883 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:51,883 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 13 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21) Word has length 45
[2025-04-28 21:21:51,883 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,884 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:51,884 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:51,884 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 120 GetRequests, 79 SyntacticMatches, 10 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 263 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=343, Invalid=713, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:51,885 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 13 mSDsluCounter, 72 mSDsCounter, 0 mSdLazyCounter, 50 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 83 SdHoareTripleChecker+Invalid, 53 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 50 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,885 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 83 Invalid, 53 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 50 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:51,886 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:51,889 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 31.
[2025-04-28 21:21:51,889 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 15 states have (on average 1.0666666666666667) internal successors, (16), 16 states have internal predecessors, (16), 3 states have call successors, (3), 2 states have call predecessors, (3), 12 states have return successors, (13), 12 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:51,890 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 32 transitions.
[2025-04-28 21:21:51,890 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 32 transitions. Word has length 45
[2025-04-28 21:21:51,890 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,890 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 32 transitions.
[2025-04-28 21:21:51,891 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 13 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:21:51,891 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 32 transitions.
[2025-04-28 21:21:51,892 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 50
[2025-04-28 21:21:51,892 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,892 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,899 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:52,096 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable8
[2025-04-28 21:21:52,096 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,097 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,097 INFO  L85        PathProgramCache]: Analyzing trace with hash -479336703, now seen corresponding path program 8 times
[2025-04-28 21:21:52,097 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,097 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1902653740]
[2025-04-28 21:21:52,097 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:52,098 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,104 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 49 statements into 2 equivalence classes.
[2025-04-28 21:21:52,116 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:21:52,116 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:52,116 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,389 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:21:52,389 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,389 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1902653740]
[2025-04-28 21:21:52,389 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1902653740] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,389 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1030370592]
[2025-04-28 21:21:52,389 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:52,389 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,391 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,393 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,397 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,589 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 49 statements into 2 equivalence classes.
[2025-04-28 21:21:52,612 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:21:52,612 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:52,612 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,613 INFO  L256         TraceCheckSpWp]: Trace formula consists of 144 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,615 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,682 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:21:52,682 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,757 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 155 refuted. 0 times theorem prover too weak. 55 trivial. 0 not checked.
[2025-04-28 21:21:59,757 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1030370592] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,758 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,758 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 15, 24] total 26
[2025-04-28 21:21:59,758 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1649049752]
[2025-04-28 21:21:59,758 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,758 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:59,758 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,759 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:59,759 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=180, Invalid=470, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:59,760 INFO  L87              Difference]: Start difference. First operand 31 states and 32 transitions. Second operand  has 26 states, 13 states have (on average 2.076923076923077) internal successors, (27), 25 states have internal predecessors, (27), 14 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (23), 11 states have call predecessors, (23), 14 states have call successors, (23)
[2025-04-28 21:21:59,930 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,930 INFO  L93              Difference]: Finished difference Result 33 states and 34 transitions.
[2025-04-28 21:21:59,932 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:21:59,933 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 13 states have (on average 2.076923076923077) internal successors, (27), 25 states have internal predecessors, (27), 14 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (23), 11 states have call predecessors, (23), 14 states have call successors, (23) Word has length 49
[2025-04-28 21:21:59,933 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,936 INFO  L225             Difference]: With dead ends: 33
[2025-04-28 21:21:59,936 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:21:59,937 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 131 GetRequests, 86 SyntacticMatches, 11 SemanticMatches, 34 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 322 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=410, Invalid=850, Unknown=0, NotChecked=0, Total=1260
[2025-04-28 21:21:59,938 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 20 mSDsluCounter, 75 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 33 SdHoareTripleChecker+Valid, 86 SdHoareTripleChecker+Invalid, 64 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,938 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [33 Valid, 86 Invalid, 64 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:59,938 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:21:59,947 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 33.
[2025-04-28 21:21:59,947 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 16 states have (on average 1.0625) internal successors, (17), 17 states have internal predecessors, (17), 3 states have call successors, (3), 2 states have call predecessors, (3), 13 states have return successors, (14), 13 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:21:59,948 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 34 transitions.
[2025-04-28 21:21:59,948 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 34 transitions. Word has length 49
[2025-04-28 21:21:59,948 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,948 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 34 transitions.
[2025-04-28 21:21:59,948 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 13 states have (on average 2.076923076923077) internal successors, (27), 25 states have internal predecessors, (27), 14 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (23), 11 states have call predecessors, (23), 14 states have call successors, (23)
[2025-04-28 21:21:59,948 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 34 transitions.
[2025-04-28 21:21:59,949 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 54
[2025-04-28 21:21:59,949 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,950 INFO  L218           NwaCegarLoop]: trace histogram [12, 11, 11, 11, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,954 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:22:00,153 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:00,153 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,153 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,153 INFO  L85        PathProgramCache]: Analyzing trace with hash 659402307, now seen corresponding path program 9 times
[2025-04-28 21:22:00,154 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,154 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1301270719]
[2025-04-28 21:22:00,154 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:00,154 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,164 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 53 statements into 12 equivalence classes.
[2025-04-28 21:22:00,191 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 12 check-sat command(s) and asserted 53 of 53 statements.
[2025-04-28 21:22:00,191 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 12 check-sat command(s)
[2025-04-28 21:22:00,191 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,510 INFO  L134       CoverageAnalysis]: Checked inductivity of 253 backedges. 0 proven. 132 refuted. 0 times theorem prover too weak. 121 trivial. 0 not checked.
[2025-04-28 21:22:00,510 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,510 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1301270719]
[2025-04-28 21:22:00,510 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1301270719] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,510 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [813715211]
[2025-04-28 21:22:00,510 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:00,510 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,513 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,515 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:00,518 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,793 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 53 statements into 12 equivalence classes.
[2025-04-28 21:22:00,830 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 12 check-sat command(s) and asserted 53 of 53 statements.
[2025-04-28 21:22:00,830 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 12 check-sat command(s)
[2025-04-28 21:22:00,830 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,832 INFO  L256         TraceCheckSpWp]: Trace formula consists of 156 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,833 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,903 INFO  L134       CoverageAnalysis]: Checked inductivity of 253 backedges. 0 proven. 132 refuted. 0 times theorem prover too weak. 121 trivial. 0 not checked.
[2025-04-28 21:22:00,903 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
