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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:44,827 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:44,887 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_61e8af8f-15f4-4ada-b14d-be3ef22f7a88/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:44,891 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:44,892 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:44,916 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:44,917 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:44,917 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:44,918 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:44,918 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:44,918 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:44,918 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:44,918 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:44,919 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:44,919 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:44,919 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:44,919 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:44,919 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:44,919 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:44,919 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:44,919 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:44,920 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:44,920 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:44,920 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:44,920 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:44,921 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:44,921 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:45,259 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:45,270 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:45,273 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:45,276 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:45,276 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:45,277 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_61e8af8f-15f4-4ada-b14d-be3ef22f7a88/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-282.smt2
[2025-04-28 21:21:45,280 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:45,287 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:45,480 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_61e8af8f-15f4-4ada-b14d-be3ef22f7a88/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-282.smt2
[2025-04-28 21:21:45,483 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:45,487 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:45,488 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:45,488 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:45,489 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:45,491 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,515 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45 Unit
[2025-04-28 21:21:45,515 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:45,516 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:45,518 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:45,518 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:45,537 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,538 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,568 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,568 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,570 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,572 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,574 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,575 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,575 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,591 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:45,595 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:45,595 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:45,595 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:45,596 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,599 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:45,616 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,634 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:45,641 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:45,651 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:45,651 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:45,651 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:45,651 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fail given in one single declaration
[2025-04-28 21:21:45,652 INFO  L130     BoogieDeclarations]: Found specification of procedure fail
[2025-04-28 21:21:45,652 INFO  L138     BoogieDeclarations]: Found implementation of procedure fail
[2025-04-28 21:21:45,652 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:45,653 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:45,653 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:45,653 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:45,653 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:45,653 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:45,706 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:45,708 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:45,790 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:45,790 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:45,802 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:45,802 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:45,803 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:45 BoogieIcfgContainer
[2025-04-28 21:21:45,803 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:45,806 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:45,806 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:45,810 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:45,811 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:45" (1/3) ...
[2025-04-28 21:21:45,811 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@32c410f0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:45, skipping insertion in model container
[2025-04-28 21:21:45,812 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (2/3) ...
[2025-04-28 21:21:45,812 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@32c410f0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:45, skipping insertion in model container
[2025-04-28 21:21:45,812 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:45" (3/3) ...
[2025-04-28 21:21:45,814 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:45,830 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:45,833 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 16 locations, 21 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:45,885 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:45,899 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;@a4847fb, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:45,899 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:45,903 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:45,912 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:45,912 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,913 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,913 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,918 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,920 INFO  L85        PathProgramCache]: Analyzing trace with hash 812378868, now seen corresponding path program 1 times
[2025-04-28 21:21:45,928 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,928 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1098879780]
[2025-04-28 21:21:45,928 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,929 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,966 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:45,987 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:45,987 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,987 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,140 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:46,141 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,141 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1098879780]
[2025-04-28 21:21:46,143 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1098879780] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,143 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,145 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:46,148 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [216810637]
[2025-04-28 21:21:46,149 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,155 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:46,155 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,186 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:46,186 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,189 INFO  L87              Difference]: Start difference. First operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:46,243 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,244 INFO  L93              Difference]: Finished difference Result 16 states and 17 transitions.
[2025-04-28 21:21:46,246 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:46,248 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:46,248 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,255 INFO  L225             Difference]: With dead ends: 16
[2025-04-28 21:21:46,255 INFO  L226             Difference]: Without dead ends: 16
[2025-04-28 21:21:46,258 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:46,262 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 1 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 35 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:46,263 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 35 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:46,278 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 16 states.
[2025-04-28 21:21:46,299 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 16 to 16.
[2025-04-28 21:21:46,300 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 16 states, 7 states have (on average 1.1428571428571428) internal successors, (8), 8 states have internal predecessors, (8), 4 states have call successors, (4), 3 states have call predecessors, (4), 4 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:46,307 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 16 states to 16 states and 17 transitions.
[2025-04-28 21:21:46,309 INFO  L79                 Accepts]: Start accepts. Automaton has 16 states and 17 transitions. Word has length 12
[2025-04-28 21:21:46,309 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,309 INFO  L485      AbstractCegarLoop]: Abstraction has 16 states and 17 transitions.
[2025-04-28 21:21:46,310 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:46,310 INFO  L278                IsEmpty]: Start isEmpty. Operand 16 states and 17 transitions.
[2025-04-28 21:21:46,311 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:46,312 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,312 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,313 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:46,314 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,314 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,314 INFO  L85        PathProgramCache]: Analyzing trace with hash 1337627512, now seen corresponding path program 1 times
[2025-04-28 21:21:46,314 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,315 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1235898649]
[2025-04-28 21:21:46,315 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,315 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,328 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:46,349 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:46,349 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,350 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,546 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:46,548 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,548 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1235898649]
[2025-04-28 21:21:46,548 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1235898649] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,549 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1080442218]
[2025-04-28 21:21:46,549 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,549 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,553 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,556 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:46,562 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,605 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:46,637 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:46,637 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,637 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,641 INFO  L256         TraceCheckSpWp]: Trace formula consists of 55 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,646 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,774 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:46,777 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,237 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:47,237 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1080442218] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,238 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,238 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:47,238 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1147893642]
[2025-04-28 21:21:47,238 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,239 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:47,239 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,240 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:47,240 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=40, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:47,240 INFO  L87              Difference]: Start difference. First operand 16 states and 17 transitions. Second operand  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:47,327 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,327 INFO  L93              Difference]: Finished difference Result 22 states and 25 transitions.
[2025-04-28 21:21:47,328 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:47,328 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6) Word has length 16
[2025-04-28 21:21:47,328 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,329 INFO  L225             Difference]: With dead ends: 22
[2025-04-28 21:21:47,329 INFO  L226             Difference]: Without dead ends: 22
[2025-04-28 21:21:47,329 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 39 GetRequests, 29 SyntacticMatches, 2 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 5 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=26, Invalid=64, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:47,330 INFO  L437           NwaCegarLoop]: 13 mSDtfsCounter, 7 mSDsluCounter, 48 mSDsCounter, 0 mSdLazyCounter, 30 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 61 SdHoareTripleChecker+Invalid, 40 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 30 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,330 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 61 Invalid, 40 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 30 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:47,331 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 22 states.
[2025-04-28 21:21:47,333 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 22 to 20.
[2025-04-28 21:21:47,334 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 20 states, 9 states have (on average 1.2222222222222223) internal successors, (11), 10 states have internal predecessors, (11), 5 states have call successors, (5), 4 states have call predecessors, (5), 5 states have return successors, (6), 5 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:47,334 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 22 transitions.
[2025-04-28 21:21:47,335 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 22 transitions. Word has length 16
[2025-04-28 21:21:47,335 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,335 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 22 transitions.
[2025-04-28 21:21:47,335 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:47,335 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 22 transitions.
[2025-04-28 21:21:47,336 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:47,336 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,336 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,341 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:47,540 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:47,540 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,541 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,541 INFO  L85        PathProgramCache]: Analyzing trace with hash 1410960252, now seen corresponding path program 2 times
[2025-04-28 21:21:47,541 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,541 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1554707579]
[2025-04-28 21:21:47,541 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,542 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,551 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:47,571 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:47,571 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,571 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,783 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:47,784 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,784 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1554707579]
[2025-04-28 21:21:47,785 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1554707579] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,785 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [483663771]
[2025-04-28 21:21:47,785 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,785 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,789 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,791 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:47,794 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,835 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:47,856 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:47,856 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,856 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,857 INFO  L256         TraceCheckSpWp]: Trace formula consists of 75 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,859 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,910 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:47,913 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,519 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:48,519 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [483663771] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,519 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,519 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 11
[2025-04-28 21:21:48,519 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1533391039]
[2025-04-28 21:21:48,520 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,520 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:48,520 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,521 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:48,521 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=84, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:48,521 INFO  L87              Difference]: Start difference. First operand 20 states and 22 transitions. Second operand  has 11 states, 5 states have (on average 2.6) internal successors, (13), 10 states have internal predecessors, (13), 7 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:48,684 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,684 INFO  L93              Difference]: Finished difference Result 30 states and 34 transitions.
[2025-04-28 21:21:48,685 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:48,685 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 5 states have (on average 2.6) internal successors, (13), 10 states have internal predecessors, (13), 7 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8) Word has length 20
[2025-04-28 21:21:48,685 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,686 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:48,686 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:48,687 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 52 GetRequests, 35 SyntacticMatches, 3 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 20 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=70, Invalid=170, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:48,688 INFO  L437           NwaCegarLoop]: 13 mSDtfsCounter, 13 mSDsluCounter, 54 mSDsCounter, 0 mSdLazyCounter, 42 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 67 SdHoareTripleChecker+Invalid, 63 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 42 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,690 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 67 Invalid, 63 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 42 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:48,691 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:48,700 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 26.
[2025-04-28 21:21:48,700 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.25) internal successors, (15), 13 states have internal predecessors, (15), 6 states have call successors, (6), 5 states have call predecessors, (6), 7 states have return successors, (9), 7 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:21:48,701 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 30 transitions.
[2025-04-28 21:21:48,701 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 30 transitions. Word has length 20
[2025-04-28 21:21:48,701 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,701 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 30 transitions.
[2025-04-28 21:21:48,701 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 5 states have (on average 2.6) internal successors, (13), 10 states have internal predecessors, (13), 7 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:48,701 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 30 transitions.
[2025-04-28 21:21:48,704 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:48,704 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,704 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,710 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:48,905 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:48,905 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,905 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,906 INFO  L85        PathProgramCache]: Analyzing trace with hash -1097944320, now seen corresponding path program 3 times
[2025-04-28 21:21:48,906 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,906 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1405197436]
[2025-04-28 21:21:48,906 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:48,906 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,913 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:48,938 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:48,938 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:48,938 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,120 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 4 proven. 10 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:49,121 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,121 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1405197436]
[2025-04-28 21:21:49,121 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1405197436] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:49,121 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [858425107]
[2025-04-28 21:21:49,122 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:49,122 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,124 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,126 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:49,131 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,174 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:49,195 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:49,195 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:49,196 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,197 INFO  L256         TraceCheckSpWp]: Trace formula consists of 95 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:49,199 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:49,255 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 4 proven. 10 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:49,255 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,231 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 4 proven. 11 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:50,231 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [858425107] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,231 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,231 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 10] total 13
[2025-04-28 21:21:50,232 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [291089148]
[2025-04-28 21:21:50,232 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,233 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:50,233 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,235 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:50,235 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:50,235 INFO  L87              Difference]: Start difference. First operand 26 states and 30 transitions. Second operand  has 13 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (10), 4 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:50,451 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,451 INFO  L93              Difference]: Finished difference Result 36 states and 44 transitions.
[2025-04-28 21:21:50,452 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:50,452 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (10), 4 states have call predecessors, (10), 8 states have call successors, (10) Word has length 24
[2025-04-28 21:21:50,452 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,453 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:50,453 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:50,453 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 62 GetRequests, 42 SyntacticMatches, 4 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 45 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=80, Invalid=226, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:50,454 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 8 mSDsluCounter, 100 mSDsCounter, 0 mSdLazyCounter, 96 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 115 SdHoareTripleChecker+Invalid, 109 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 96 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,454 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 115 Invalid, 109 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 96 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:50,455 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:50,463 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 28.
[2025-04-28 21:21:50,463 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 13 states have (on average 1.1538461538461537) internal successors, (15), 14 states have internal predecessors, (15), 7 states have call successors, (7), 6 states have call predecessors, (7), 7 states have return successors, (9), 7 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:50,464 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 31 transitions.
[2025-04-28 21:21:50,464 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 31 transitions. Word has length 24
[2025-04-28 21:21:50,465 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,465 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 31 transitions.
[2025-04-28 21:21:50,465 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (10), 4 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:50,465 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 31 transitions.
[2025-04-28 21:21:50,466 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:50,466 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,466 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,472 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:50,666 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:50,666 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,667 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,667 INFO  L85        PathProgramCache]: Analyzing trace with hash 306702852, now seen corresponding path program 4 times
[2025-04-28 21:21:50,667 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,667 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [551509891]
[2025-04-28 21:21:50,667 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:50,667 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,676 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:50,701 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:50,702 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:50,702 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,009 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 25 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:51,009 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,009 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [551509891]
[2025-04-28 21:21:51,009 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [551509891] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:51,009 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1218474469]
[2025-04-28 21:21:51,009 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:51,010 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,012 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:51,014 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:51,018 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:51,056 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:51,076 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:51,076 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:51,076 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,077 INFO  L256         TraceCheckSpWp]: Trace formula consists of 115 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:51,079 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:51,147 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:51,148 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,616 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 26 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:52,616 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1218474469] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,616 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,616 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 10, 12] total 17
[2025-04-28 21:21:52,617 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1695805197]
[2025-04-28 21:21:52,617 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,618 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:52,618 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,619 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:52,619 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=61, Invalid=211, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:52,619 INFO  L87              Difference]: Start difference. First operand 28 states and 31 transitions. Second operand  has 17 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (13), 5 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:52,802 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,804 INFO  L93              Difference]: Finished difference Result 36 states and 41 transitions.
[2025-04-28 21:21:52,805 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:52,809 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (13), 5 states have call predecessors, (13), 10 states have call successors, (13) Word has length 28
[2025-04-28 21:21:52,810 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,810 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:52,810 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:52,811 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 73 GetRequests, 47 SyntacticMatches, 5 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 112 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=145, Invalid=361, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:52,811 INFO  L437           NwaCegarLoop]: 13 mSDtfsCounter, 16 mSDsluCounter, 106 mSDsCounter, 0 mSdLazyCounter, 72 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 119 SdHoareTripleChecker+Invalid, 94 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 72 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,811 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 119 Invalid, 94 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 72 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:52,812 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:52,815 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 32.
[2025-04-28 21:21:52,819 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 15 states have (on average 1.1333333333333333) internal successors, (17), 16 states have internal predecessors, (17), 7 states have call successors, (7), 6 states have call predecessors, (7), 9 states have return successors, (11), 9 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:52,820 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 35 transitions.
[2025-04-28 21:21:52,821 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 35 transitions. Word has length 28
[2025-04-28 21:21:52,821 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,821 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 35 transitions.
[2025-04-28 21:21:52,823 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (13), 5 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:52,823 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 35 transitions.
[2025-04-28 21:21:52,824 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:52,824 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,824 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,831 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:53,025 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:53,025 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,026 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,026 INFO  L85        PathProgramCache]: Analyzing trace with hash 822478476, now seen corresponding path program 5 times
[2025-04-28 21:21:53,026 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,026 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [251590733]
[2025-04-28 21:21:53,026 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:53,026 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,037 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:53,607 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:53,607 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:53,607 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,948 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 51 refuted. 0 times theorem prover too weak. 27 trivial. 0 not checked.
[2025-04-28 21:21:53,948 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,949 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [251590733]
[2025-04-28 21:21:53,949 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [251590733] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,949 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1000573359]
[2025-04-28 21:21:53,949 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:53,949 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,951 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,953 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:53,957 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,017 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:54,060 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:54,060 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:54,060 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,062 INFO  L256         TraceCheckSpWp]: Trace formula consists of 155 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,064 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,147 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 51 refuted. 0 times theorem prover too weak. 27 trivial. 0 not checked.
[2025-04-28 21:21:54,148 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:57,186 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 57 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:21:57,186 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1000573359] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:57,187 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:57,187 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 16] total 19
[2025-04-28 21:21:57,187 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2035085222]
[2025-04-28 21:21:57,187 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,188 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:57,188 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,188 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:57,189 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=66, Invalid=276, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:57,189 INFO  L87              Difference]: Start difference. First operand 32 states and 35 transitions. Second operand  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:57,406 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,406 INFO  L93              Difference]: Finished difference Result 40 states and 45 transitions.
[2025-04-28 21:21:57,406 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:57,406 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16) Word has length 36
[2025-04-28 21:21:57,407 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,407 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:21:57,408 INFO  L226             Difference]: Without dead ends: 38
[2025-04-28 21:21:57,408 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 96 GetRequests, 63 SyntacticMatches, 7 SemanticMatches, 26 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 138 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=218, Invalid=538, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:57,409 INFO  L437           NwaCegarLoop]: 13 mSDtfsCounter, 32 mSDsluCounter, 90 mSDsCounter, 0 mSdLazyCounter, 56 mSolverCounterSat, 43 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 33 SdHoareTripleChecker+Valid, 103 SdHoareTripleChecker+Invalid, 99 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 43 IncrementalHoareTripleChecker+Valid, 56 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,409 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [33 Valid, 103 Invalid, 99 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [43 Valid, 56 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:57,410 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 38 states.
[2025-04-28 21:21:57,414 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 38 to 36.
[2025-04-28 21:21:57,415 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 17 states have (on average 1.1176470588235294) internal successors, (19), 18 states have internal predecessors, (19), 7 states have call successors, (7), 6 states have call predecessors, (7), 11 states have return successors, (13), 11 states have call predecessors, (13), 7 states have call successors, (13)
[2025-04-28 21:21:57,415 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 39 transitions.
[2025-04-28 21:21:57,415 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 39 transitions. Word has length 36
[2025-04-28 21:21:57,416 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,416 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 39 transitions.
[2025-04-28 21:21:57,416 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:57,416 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 39 transitions.
[2025-04-28 21:21:57,417 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:57,417 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,417 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,422 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:57,621 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:57,621 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,622 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,622 INFO  L85        PathProgramCache]: Analyzing trace with hash 1491263764, now seen corresponding path program 6 times
[2025-04-28 21:21:57,622 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,622 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [435590001]
[2025-04-28 21:21:57,622 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:57,622 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,632 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 44 statements into 9 equivalence classes.
[2025-04-28 21:21:57,735 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 9 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:57,735 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 9 check-sat command(s)
[2025-04-28 21:21:57,735 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,071 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 88 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:21:58,072 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,072 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [435590001]
[2025-04-28 21:21:58,072 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [435590001] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,072 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [140575253]
[2025-04-28 21:21:58,072 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:58,072 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,074 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:58,076 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:58,079 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,164 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 44 statements into 9 equivalence classes.
[2025-04-28 21:21:58,233 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 9 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:58,233 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 9 check-sat command(s)
[2025-04-28 21:21:58,233 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,235 INFO  L256         TraceCheckSpWp]: Trace formula consists of 195 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,237 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,312 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 88 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:21:58,314 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:03,484 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:22:03,485 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [140575253] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:03,485 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:03,485 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 20] total 23
[2025-04-28 21:22:03,485 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1062442569]
[2025-04-28 21:22:03,485 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,486 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:22:03,486 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,487 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:22:03,487 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=92, Invalid=414, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:22:03,487 INFO  L87              Difference]: Start difference. First operand 36 states and 39 transitions. Second operand  has 23 states, 11 states have (on average 2.272727272727273) internal successors, (25), 22 states have internal predecessors, (25), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (20), 9 states have call predecessors, (20), 13 states have call successors, (20)
[2025-04-28 21:22:03,717 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,718 INFO  L93              Difference]: Finished difference Result 44 states and 49 transitions.
[2025-04-28 21:22:03,718 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:22:03,719 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 11 states have (on average 2.272727272727273) internal successors, (25), 22 states have internal predecessors, (25), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (20), 9 states have call predecessors, (20), 13 states have call successors, (20) Word has length 44
[2025-04-28 21:22:03,719 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,719 INFO  L225             Difference]: With dead ends: 44
[2025-04-28 21:22:03,720 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:22:03,720 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 118 GetRequests, 77 SyntacticMatches, 9 SemanticMatches, 32 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 239 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=322, Invalid=800, Unknown=0, NotChecked=0, Total=1122
[2025-04-28 21:22:03,721 INFO  L437           NwaCegarLoop]: 13 mSDtfsCounter, 40 mSDsluCounter, 100 mSDsCounter, 0 mSdLazyCounter, 61 mSolverCounterSat, 54 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 41 SdHoareTripleChecker+Valid, 113 SdHoareTripleChecker+Invalid, 115 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 54 IncrementalHoareTripleChecker+Valid, 61 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,721 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [41 Valid, 113 Invalid, 115 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [54 Valid, 61 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:03,722 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:22:03,727 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 40.
[2025-04-28 21:22:03,727 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 19 states have (on average 1.105263157894737) internal successors, (21), 20 states have internal predecessors, (21), 7 states have call successors, (7), 6 states have call predecessors, (7), 13 states have return successors, (15), 13 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:22:03,728 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 43 transitions.
[2025-04-28 21:22:03,728 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 43 transitions. Word has length 44
[2025-04-28 21:22:03,728 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,728 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 43 transitions.
[2025-04-28 21:22:03,728 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 11 states have (on average 2.272727272727273) internal successors, (25), 22 states have internal predecessors, (25), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (20), 9 states have call predecessors, (20), 13 states have call successors, (20)
[2025-04-28 21:22:03,728 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 43 transitions.
[2025-04-28 21:22:03,729 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:22:03,729 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,729 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,734 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:22:03,933 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:22:03,933 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:03,934 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:03,934 INFO  L85        PathProgramCache]: Analyzing trace with hash -722634340, now seen corresponding path program 7 times
[2025-04-28 21:22:03,934 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:03,934 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [143236563]
[2025-04-28 21:22:03,934 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:03,934 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:03,956 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:22:03,997 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:22:03,997 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,997 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,118 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:22:07,119 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,119 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [143236563]
[2025-04-28 21:22:07,119 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [143236563] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,119 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1469792489]
[2025-04-28 21:22:07,119 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:07,119 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,121 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:07,124 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:07,127 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,273 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 52 statements into 1 equivalence classes.
[2025-04-28 21:22:07,320 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:22:07,320 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,320 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,327 WARN  L254         TraceCheckSpWp]: Trace formula consists of 235 conjuncts, 130 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,336 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
