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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:25,271 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:25,369 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5d1ad64f-1354-48ce-9c7d-c214291ec57e/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:25,378 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:25,381 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:25,420 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:25,421 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:25,422 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:25,422 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:25,422 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:25,424 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:25,424 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:25,424 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:25,424 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:25,424 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:25,424 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:25,425 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:25,425 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:25,425 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:25,426 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:25,426 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:25,426 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:25,426 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:25,426 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:25,426 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:25,427 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:25,427 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:25,793 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:25,804 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:25,807 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:25,810 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:25,811 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:25,812 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5d1ad64f-1354-48ce-9c7d-c214291ec57e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-075.smt2
[2025-04-28 21:21:25,814 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:25,818 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:26,016 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5d1ad64f-1354-48ce-9c7d-c214291ec57e/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-075.smt2
[2025-04-28 21:21:26,020 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:26,023 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:26,025 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:26,025 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:26,025 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:26,030 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,055 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26 Unit
[2025-04-28 21:21:26,055 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:26,057 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:26,058 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:26,058 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:26,074 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,074 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,098 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,100 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,102 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,104 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,106 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,107 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,108 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,125 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:26,127 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:26,127 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:26,128 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:26,129 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,132 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:26,149 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:26,163 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:26,170 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:26,180 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:26,181 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:26,181 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:26,181 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:26,181 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:26,181 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:26,181 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:26,182 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:26,182 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:26,225 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:26,227 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:26,285 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:26,285 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:26,296 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:26,296 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:26,297 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:26 BoogieIcfgContainer
[2025-04-28 21:21:26,297 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:26,300 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:26,300 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:26,304 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:26,305 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:26" (1/3) ...
[2025-04-28 21:21:26,306 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4992494c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:26, skipping insertion in model container
[2025-04-28 21:21:26,306 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (2/3) ...
[2025-04-28 21:21:26,306 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4992494c and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:26, skipping insertion in model container
[2025-04-28 21:21:26,306 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:26" (3/3) ...
[2025-04-28 21:21:26,308 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:26,323 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:26,326 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:26,376 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:26,400 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;@a1ad803, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:26,400 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:26,406 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:26,415 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:26,415 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,416 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,416 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,424 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,425 INFO  L85        PathProgramCache]: Analyzing trace with hash -1586659766, now seen corresponding path program 1 times
[2025-04-28 21:21:26,433 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,433 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1393210491]
[2025-04-28 21:21:26,434 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,434 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,459 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:26,480 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:26,481 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,481 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,660 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:26,661 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,661 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1393210491]
[2025-04-28 21:21:26,662 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1393210491] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:26,662 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:26,666 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:26,668 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1232605085]
[2025-04-28 21:21:26,671 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,676 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:26,676 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,710 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:26,710 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:26,712 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:26,774 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,774 INFO  L93              Difference]: Finished difference Result 13 states and 14 transitions.
[2025-04-28 21:21:26,780 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:26,781 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:26,782 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,793 INFO  L225             Difference]: With dead ends: 13
[2025-04-28 21:21:26,793 INFO  L226             Difference]: Without dead ends: 13
[2025-04-28 21:21:26,795 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:26,800 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:26,801 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:26,813 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 13 states.
[2025-04-28 21:21:26,832 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 13 to 13.
[2025-04-28 21:21:26,833 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:26,839 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 13 states to 13 states and 14 transitions.
[2025-04-28 21:21:26,843 INFO  L79                 Accepts]: Start accepts. Automaton has 13 states and 14 transitions. Word has length 9
[2025-04-28 21:21:26,843 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,843 INFO  L485      AbstractCegarLoop]: Abstraction has 13 states and 14 transitions.
[2025-04-28 21:21:26,843 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:26,844 INFO  L278                IsEmpty]: Start isEmpty. Operand 13 states and 14 transitions.
[2025-04-28 21:21:26,845 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:26,845 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,845 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,845 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:26,846 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,846 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,846 INFO  L85        PathProgramCache]: Analyzing trace with hash 1339989006, now seen corresponding path program 1 times
[2025-04-28 21:21:26,846 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,846 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1566004993]
[2025-04-28 21:21:26,846 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,847 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,858 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:26,876 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:26,876 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,876 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,077 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:27,077 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,077 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1566004993]
[2025-04-28 21:21:27,077 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1566004993] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,077 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [755225970]
[2025-04-28 21:21:27,078 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,078 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,080 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,087 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:27,090 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:27,135 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:27,149 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:27,150 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,150 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,152 INFO  L256         TraceCheckSpWp]: Trace formula consists of 49 conjuncts, 6 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:27,156 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,368 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:27,369 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:27,950 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:27,950 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [755225970] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:27,950 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:27,951 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:27,951 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1664507797]
[2025-04-28 21:21:27,953 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,954 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:27,955 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,955 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:27,956 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=38, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:27,956 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:28,026 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,026 INFO  L93              Difference]: Finished difference Result 15 states and 16 transitions.
[2025-04-28 21:21:28,026 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:28,027 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:28,027 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,027 INFO  L225             Difference]: With dead ends: 15
[2025-04-28 21:21:28,028 INFO  L226             Difference]: Without dead ends: 15
[2025-04-28 21:21:28,029 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 22 SyntacticMatches, 3 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=49, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:28,030 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:28,032 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:28,033 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15 states.
[2025-04-28 21:21:28,035 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15 to 15.
[2025-04-28 21:21:28,035 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:28,036 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 15 states to 15 states and 16 transitions.
[2025-04-28 21:21:28,036 INFO  L79                 Accepts]: Start accepts. Automaton has 15 states and 16 transitions. Word has length 13
[2025-04-28 21:21:28,036 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,036 INFO  L485      AbstractCegarLoop]: Abstraction has 15 states and 16 transitions.
[2025-04-28 21:21:28,038 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:28,039 INFO  L278                IsEmpty]: Start isEmpty. Operand 15 states and 16 transitions.
[2025-04-28 21:21:28,039 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:28,039 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,039 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,045 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:28,244 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:28,244 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,244 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,244 INFO  L85        PathProgramCache]: Analyzing trace with hash -1013855662, now seen corresponding path program 2 times
[2025-04-28 21:21:28,245 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,245 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [527251101]
[2025-04-28 21:21:28,245 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:28,245 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,252 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:28,268 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:28,268 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:28,268 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,474 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:28,474 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,474 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [527251101]
[2025-04-28 21:21:28,474 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [527251101] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,474 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [993741209]
[2025-04-28 21:21:28,474 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:28,475 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,477 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,479 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:28,482 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,520 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:28,540 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:28,540 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:28,541 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,542 INFO  L256         TraceCheckSpWp]: Trace formula consists of 69 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,543 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,625 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:28,626 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:29,356 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:29,356 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [993741209] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:29,356 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:29,356 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 10
[2025-04-28 21:21:29,357 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [963744798]
[2025-04-28 21:21:29,357 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,357 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:29,357 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,358 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:29,358 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:29,358 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:29,417 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,417 INFO  L93              Difference]: Finished difference Result 17 states and 18 transitions.
[2025-04-28 21:21:29,418 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:29,418 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:29,419 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,419 INFO  L225             Difference]: With dead ends: 17
[2025-04-28 21:21:29,419 INFO  L226             Difference]: Without dead ends: 17
[2025-04-28 21:21:29,420 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 43 GetRequests, 29 SyntacticMatches, 4 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=42, Invalid=90, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:29,420 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:29,421 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:29,421 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17 states.
[2025-04-28 21:21:29,424 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 17 to 17.
[2025-04-28 21:21:29,424 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:29,425 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 18 transitions.
[2025-04-28 21:21:29,425 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 18 transitions. Word has length 17
[2025-04-28 21:21:29,425 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,425 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 18 transitions.
[2025-04-28 21:21:29,425 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:29,425 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 18 transitions.
[2025-04-28 21:21:29,426 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:29,426 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,426 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:29,432 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:29,627 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:29,627 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,627 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,628 INFO  L85        PathProgramCache]: Analyzing trace with hash 447752470, now seen corresponding path program 3 times
[2025-04-28 21:21:29,628 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,628 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1357454214]
[2025-04-28 21:21:29,628 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:29,628 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,637 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:29,677 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:29,680 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:29,681 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,975 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 14 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:29,976 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,976 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1357454214]
[2025-04-28 21:21:29,976 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1357454214] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,976 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [886955510]
[2025-04-28 21:21:29,976 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:29,976 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,979 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,981 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:29,985 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:30,022 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:30,042 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,042 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:30,042 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,043 INFO  L256         TraceCheckSpWp]: Trace formula consists of 89 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:30,045 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,108 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:30,109 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:31,281 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:31,282 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [886955510] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:31,282 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:31,282 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 8, 10] total 14
[2025-04-28 21:21:31,282 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1753643572]
[2025-04-28 21:21:31,282 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,283 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:31,283 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,284 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:31,285 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=52, Invalid=130, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:31,286 INFO  L87              Difference]: Start difference. First operand 17 states and 18 transitions. Second operand  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 4 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:31,404 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,407 INFO  L93              Difference]: Finished difference Result 19 states and 20 transitions.
[2025-04-28 21:21:31,407 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:31,408 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 4 states have call predecessors, (10), 8 states have call successors, (10) Word has length 21
[2025-04-28 21:21:31,408 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,408 INFO  L225             Difference]: With dead ends: 19
[2025-04-28 21:21:31,408 INFO  L226             Difference]: Without dead ends: 19
[2025-04-28 21:21:31,409 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 34 SyntacticMatches, 5 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 65 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=82, Invalid=190, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:31,409 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 15 mSDsluCounter, 56 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 14 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 67 SdHoareTripleChecker+Invalid, 53 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 14 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,410 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 67 Invalid, 53 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [14 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:31,411 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 19 states.
[2025-04-28 21:21:31,415 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 19 to 19.
[2025-04-28 21:21:31,415 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 19 states, 9 states have (on average 1.1111111111111112) internal successors, (10), 10 states have internal predecessors, (10), 3 states have call successors, (3), 2 states have call predecessors, (3), 6 states have return successors, (7), 6 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:31,416 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 19 states to 19 states and 20 transitions.
[2025-04-28 21:21:31,416 INFO  L79                 Accepts]: Start accepts. Automaton has 19 states and 20 transitions. Word has length 21
[2025-04-28 21:21:31,416 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,417 INFO  L485      AbstractCegarLoop]: Abstraction has 19 states and 20 transitions.
[2025-04-28 21:21:31,418 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 4 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:31,418 INFO  L278                IsEmpty]: Start isEmpty. Operand 19 states and 20 transitions.
[2025-04-28 21:21:31,419 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:31,420 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,420 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,426 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:31,624 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:31,624 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,624 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,625 INFO  L85        PathProgramCache]: Analyzing trace with hash -436545446, now seen corresponding path program 4 times
[2025-04-28 21:21:31,625 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,625 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1831293972]
[2025-04-28 21:21:31,625 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:31,625 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,631 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:31,645 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:31,645 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:31,645 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,866 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:31,866 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,866 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1831293972]
[2025-04-28 21:21:31,866 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1831293972] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,867 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1340144601]
[2025-04-28 21:21:31,867 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:31,867 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,869 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,871 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:31,876 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,925 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:31,947 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:31,947 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:31,947 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,948 INFO  L256         TraceCheckSpWp]: Trace formula consists of 109 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,950 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,067 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:32,067 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,661 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:33,662 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1340144601] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,662 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,662 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 12] total 14
[2025-04-28 21:21:33,662 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [574218785]
[2025-04-28 21:21:33,662 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,663 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:33,663 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,663 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:33,664 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=128, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:33,664 INFO  L87              Difference]: Start difference. First operand 19 states and 20 transitions. Second operand  has 14 states, 7 states have (on average 2.142857142857143) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:33,757 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,757 INFO  L93              Difference]: Finished difference Result 21 states and 22 transitions.
[2025-04-28 21:21:33,758 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:33,758 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.142857142857143) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11) Word has length 25
[2025-04-28 21:21:33,758 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,759 INFO  L225             Difference]: With dead ends: 21
[2025-04-28 21:21:33,759 INFO  L226             Difference]: Without dead ends: 21
[2025-04-28 21:21:33,759 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 65 GetRequests, 43 SyntacticMatches, 6 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 33 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=98, Invalid=208, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:33,760 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 11 mSDsluCounter, 39 mSDsCounter, 0 mSdLazyCounter, 29 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 50 SdHoareTripleChecker+Invalid, 35 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 29 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,760 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 50 Invalid, 35 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 29 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:33,761 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 21 states.
[2025-04-28 21:21:33,763 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 21 to 21.
[2025-04-28 21:21:33,764 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:33,764 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 21 states to 21 states and 22 transitions.
[2025-04-28 21:21:33,764 INFO  L79                 Accepts]: Start accepts. Automaton has 21 states and 22 transitions. Word has length 25
[2025-04-28 21:21:33,765 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,765 INFO  L485      AbstractCegarLoop]: Abstraction has 21 states and 22 transitions.
[2025-04-28 21:21:33,765 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.142857142857143) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:33,766 INFO  L278                IsEmpty]: Start isEmpty. Operand 21 states and 22 transitions.
[2025-04-28 21:21:33,767 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:33,767 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,767 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,772 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:33,968 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:33,968 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,968 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,969 INFO  L85        PathProgramCache]: Analyzing trace with hash -1295321058, now seen corresponding path program 5 times
[2025-04-28 21:21:33,969 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,969 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1943316387]
[2025-04-28 21:21:33,969 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:33,969 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,978 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 29 statements into 6 equivalence classes.
[2025-04-28 21:21:34,033 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:34,034 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:34,034 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,218 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:34,218 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,218 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1943316387]
[2025-04-28 21:21:34,219 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1943316387] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,219 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1242109912]
[2025-04-28 21:21:34,219 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:34,219 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,221 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,223 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:34,236 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,291 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 29 statements into 6 equivalence classes.
[2025-04-28 21:21:34,321 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:34,322 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:34,322 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,323 INFO  L256         TraceCheckSpWp]: Trace formula consists of 129 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,326 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,430 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:34,430 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:36,654 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:36,655 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1242109912] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:36,655 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:36,655 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 14] total 16
[2025-04-28 21:21:36,655 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2110075998]
[2025-04-28 21:21:36,655 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,656 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:36,656 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,656 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:36,657 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=70, Invalid=170, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:36,657 INFO  L87              Difference]: Start difference. First operand 21 states and 22 transitions. Second operand  has 16 states, 8 states have (on average 2.125) internal successors, (17), 15 states have internal predecessors, (17), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:36,779 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,780 INFO  L93              Difference]: Finished difference Result 23 states and 24 transitions.
[2025-04-28 21:21:36,780 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:36,781 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.125) internal successors, (17), 15 states have internal predecessors, (17), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13) Word has length 29
[2025-04-28 21:21:36,781 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,782 INFO  L225             Difference]: With dead ends: 23
[2025-04-28 21:21:36,782 INFO  L226             Difference]: Without dead ends: 23
[2025-04-28 21:21:36,782 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 76 GetRequests, 50 SyntacticMatches, 7 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 51 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=135, Invalid=285, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:36,783 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 22 mSDsluCounter, 53 mSDsCounter, 0 mSdLazyCounter, 35 mSolverCounterSat, 20 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 30 SdHoareTripleChecker+Valid, 64 SdHoareTripleChecker+Invalid, 55 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 20 IncrementalHoareTripleChecker+Valid, 35 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,783 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [30 Valid, 64 Invalid, 55 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [20 Valid, 35 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,784 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 23 states.
[2025-04-28 21:21:36,786 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 23 to 23.
[2025-04-28 21:21:36,787 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 23 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 3 states have call successors, (3), 2 states have call predecessors, (3), 8 states have return successors, (9), 8 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:36,787 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 23 states to 23 states and 24 transitions.
[2025-04-28 21:21:36,788 INFO  L79                 Accepts]: Start accepts. Automaton has 23 states and 24 transitions. Word has length 29
[2025-04-28 21:21:36,788 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,788 INFO  L485      AbstractCegarLoop]: Abstraction has 23 states and 24 transitions.
[2025-04-28 21:21:36,788 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.125) internal successors, (17), 15 states have internal predecessors, (17), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:36,788 INFO  L278                IsEmpty]: Start isEmpty. Operand 23 states and 24 transitions.
[2025-04-28 21:21:36,789 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:36,789 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,789 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,794 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:36,992 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:36,992 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,992 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,992 INFO  L85        PathProgramCache]: Analyzing trace with hash 353478754, now seen corresponding path program 6 times
[2025-04-28 21:21:36,992 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,993 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [433202800]
[2025-04-28 21:21:36,993 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:36,993 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,002 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:37,042 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:37,043 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:37,043 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,361 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 3 proven. 44 refuted. 0 times theorem prover too weak. 31 trivial. 0 not checked.
[2025-04-28 21:21:37,361 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,361 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [433202800]
[2025-04-28 21:21:37,361 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [433202800] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,361 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [829225209]
[2025-04-28 21:21:37,361 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:37,361 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,364 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,366 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:37,369 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,446 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:37,478 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:37,478 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:37,478 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,479 INFO  L256         TraceCheckSpWp]: Trace formula consists of 149 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,481 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,592 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 42 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:37,593 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,315 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:40,315 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [829225209] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,315 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,315 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 16] total 19
[2025-04-28 21:21:40,315 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1589219540]
[2025-04-28 21:21:40,315 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,316 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:40,316 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,317 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:40,317 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=97, Invalid=245, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:40,317 INFO  L87              Difference]: Start difference. First operand 23 states and 24 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, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:40,470 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,470 INFO  L93              Difference]: Finished difference Result 25 states and 26 transitions.
[2025-04-28 21:21:40,472 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:40,473 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, (16), 7 states have call predecessors, (16), 11 states have call successors, (16) Word has length 33
[2025-04-28 21:21:40,473 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,474 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:21:40,474 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:21:40,474 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 87 GetRequests, 56 SyntacticMatches, 8 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 100 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=193, Invalid=407, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:40,475 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 25 mSDsluCounter, 59 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 70 SdHoareTripleChecker+Invalid, 64 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,475 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 70 Invalid, 64 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:40,480 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:21:40,483 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 25.
[2025-04-28 21:21:40,483 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:40,487 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 26 transitions.
[2025-04-28 21:21:40,487 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 26 transitions. Word has length 33
[2025-04-28 21:21:40,487 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,487 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 26 transitions.
[2025-04-28 21:21:40,487 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, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:40,487 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 26 transitions.
[2025-04-28 21:21:40,488 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:40,488 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,488 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,496 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:40,688 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:40,689 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,689 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,689 INFO  L85        PathProgramCache]: Analyzing trace with hash 827853094, now seen corresponding path program 7 times
[2025-04-28 21:21:40,689 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,689 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [213249871]
[2025-04-28 21:21:40,689 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:40,689 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,695 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:40,717 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:40,718 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,718 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,993 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:40,994 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,994 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [213249871]
[2025-04-28 21:21:40,994 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [213249871] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,994 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1104264717]
[2025-04-28 21:21:40,994 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:40,994 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,997 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,999 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:41,003 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,101 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:41,132 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:41,133 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,133 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,140 INFO  L256         TraceCheckSpWp]: Trace formula consists of 169 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,141 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,270 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:41,270 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,115 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:45,115 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1104264717] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,116 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,116 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 18] total 20
[2025-04-28 21:21:45,116 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [716698761]
[2025-04-28 21:21:45,116 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,116 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:45,116 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,117 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:45,117 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=108, Invalid=272, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:45,118 INFO  L87              Difference]: Start difference. First operand 25 states and 26 transitions. Second operand  has 20 states, 10 states have (on average 2.1) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:45,275 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,275 INFO  L93              Difference]: Finished difference Result 27 states and 28 transitions.
[2025-04-28 21:21:45,275 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:45,276 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.1) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17) Word has length 37
[2025-04-28 21:21:45,276 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,277 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:45,277 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:45,279 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 98 GetRequests, 64 SyntacticMatches, 9 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 99 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=227, Invalid=475, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:45,279 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 32 mSDsluCounter, 67 mSDsCounter, 0 mSdLazyCounter, 50 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 42 SdHoareTripleChecker+Valid, 78 SdHoareTripleChecker+Invalid, 78 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 50 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,280 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [42 Valid, 78 Invalid, 78 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 50 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,281 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:45,286 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:45,290 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:45,290 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 28 transitions.
[2025-04-28 21:21:45,290 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 28 transitions. Word has length 37
[2025-04-28 21:21:45,292 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,292 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 28 transitions.
[2025-04-28 21:21:45,292 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.1) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:45,292 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 28 transitions.
[2025-04-28 21:21:45,293 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:45,294 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,294 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,298 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:45,495 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:45,495 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,495 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,495 INFO  L85        PathProgramCache]: Analyzing trace with hash -960546198, now seen corresponding path program 8 times
[2025-04-28 21:21:45,495 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,495 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1825473405]
[2025-04-28 21:21:45,496 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:45,496 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,502 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 41 statements into 2 equivalence classes.
[2025-04-28 21:21:45,520 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:45,520 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:45,520 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,803 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:45,803 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,803 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1825473405]
[2025-04-28 21:21:45,803 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1825473405] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,803 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [896457399]
[2025-04-28 21:21:45,803 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:45,803 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,806 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,808 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:45,811 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,949 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 41 statements into 2 equivalence classes.
[2025-04-28 21:21:45,979 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:45,980 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:45,980 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,986 INFO  L256         TraceCheckSpWp]: Trace formula consists of 189 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,988 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,128 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:46,128 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,202 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:51,203 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [896457399] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,203 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,203 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 20] total 22
[2025-04-28 21:21:51,203 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [131601643]
[2025-04-28 21:21:51,203 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,203 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:51,204 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,204 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:51,205 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=130, Invalid=332, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:51,205 INFO  L87              Difference]: Start difference. First operand 27 states and 28 transitions. Second operand  has 22 states, 11 states have (on average 2.090909090909091) internal successors, (23), 21 states have internal predecessors, (23), 12 states have call successors, (12), 1 states have call predecessors, (12), 10 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19)
[2025-04-28 21:21:51,404 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,405 INFO  L93              Difference]: Finished difference Result 29 states and 30 transitions.
[2025-04-28 21:21:51,405 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:51,405 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 2.090909090909091) internal successors, (23), 21 states have internal predecessors, (23), 12 states have call successors, (12), 1 states have call predecessors, (12), 10 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19) Word has length 41
[2025-04-28 21:21:51,406 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,406 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:51,409 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:21:51,410 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 109 GetRequests, 71 SyntacticMatches, 10 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 129 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=282, Invalid=588, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:51,411 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 47 mSDsluCounter, 63 mSDsCounter, 0 mSdLazyCounter, 48 mSolverCounterSat, 45 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 58 SdHoareTripleChecker+Valid, 74 SdHoareTripleChecker+Invalid, 93 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 45 IncrementalHoareTripleChecker+Valid, 48 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,411 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [58 Valid, 74 Invalid, 93 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [45 Valid, 48 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:51,411 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:21:51,418 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:21:51,418 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:51,419 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 30 transitions.
[2025-04-28 21:21:51,419 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 30 transitions. Word has length 41
[2025-04-28 21:21:51,419 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,419 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 30 transitions.
[2025-04-28 21:21:51,419 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 2.090909090909091) internal successors, (23), 21 states have internal predecessors, (23), 12 states have call successors, (12), 1 states have call predecessors, (12), 10 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19)
[2025-04-28 21:21:51,420 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 30 transitions.
[2025-04-28 21:21:51,420 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:21:51,420 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,420 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,429 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:51,624 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:21:51,624 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,625 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,625 INFO  L85        PathProgramCache]: Analyzing trace with hash -1191158738, now seen corresponding path program 9 times
[2025-04-28 21:21:51,625 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,625 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [82309730]
[2025-04-28 21:21:51,625 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:51,625 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,648 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 45 statements into 10 equivalence classes.
[2025-04-28 21:21:51,718 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:51,719 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:51,719 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,252 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 98 refuted. 0 times theorem prover too weak. 73 trivial. 0 not checked.
[2025-04-28 21:21:52,253 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,253 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [82309730]
[2025-04-28 21:21:52,253 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [82309730] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,253 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1499109566]
[2025-04-28 21:21:52,253 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:52,253 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,257 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,259 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,263 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,455 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 45 statements into 10 equivalence classes.
[2025-04-28 21:21:52,499 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:52,499 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:52,499 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,501 INFO  L256         TraceCheckSpWp]: Trace formula consists of 209 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,503 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,580 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:52,580 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,359 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:59,359 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1499109566] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,359 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,359 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 14, 22] total 25
[2025-04-28 21:21:59,359 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1393739747]
[2025-04-28 21:21:59,359 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,360 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:21:59,360 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,361 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:21:59,361 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=175, Invalid=425, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:59,361 INFO  L87              Difference]: Start difference. First operand 29 states and 30 transitions. Second operand  has 25 states, 13 states have (on average 2.076923076923077) internal successors, (27), 24 states have internal predecessors, (27), 13 states have call successors, (13), 1 states have call predecessors, (13), 12 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:21:59,536 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,537 INFO  L93              Difference]: Finished difference Result 31 states and 32 transitions.
[2025-04-28 21:21:59,538 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:59,539 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 13 states have (on average 2.076923076923077) internal successors, (27), 24 states have internal predecessors, (27), 13 states have call successors, (13), 1 states have call predecessors, (13), 12 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:59,539 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,539 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:59,539 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:59,540 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 120 GetRequests, 77 SyntacticMatches, 11 SemanticMatches, 32 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 322 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=373, Invalid=749, Unknown=0, NotChecked=0, Total=1122
[2025-04-28 21:21:59,541 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 33 mSDsluCounter, 80 mSDsCounter, 0 mSdLazyCounter, 58 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 45 SdHoareTripleChecker+Valid, 91 SdHoareTripleChecker+Invalid, 84 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 58 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,541 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [45 Valid, 91 Invalid, 84 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 58 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:59,541 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:59,546 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 31.
[2025-04-28 21:21:59,546 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:59,547 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 32 transitions.
[2025-04-28 21:21:59,547 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 32 transitions. Word has length 45
[2025-04-28 21:21:59,547 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,547 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 32 transitions.
[2025-04-28 21:21:59,548 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 13 states have (on average 2.076923076923077) internal successors, (27), 24 states have internal predecessors, (27), 13 states have call successors, (13), 1 states have call predecessors, (13), 12 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:21:59,548 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 32 transitions.
[2025-04-28 21:21:59,548 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 50
[2025-04-28 21:21:59,549 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,549 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,558 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
