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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:40,252 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:40,348 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a50a24b8-b322-45b5-a60a-f8e32f8daba2/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:40,356 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:40,357 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:40,379 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:40,380 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:40,380 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:40,380 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:40,380 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:40,380 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:40,381 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:40,381 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:40,381 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:40,381 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:40,381 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:40,381 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:40,381 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:40,381 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,382 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:40,382 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:40,382 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:40,382 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:40,382 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:40,382 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:40,383 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:40,383 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:40,741 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:40,753 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:40,755 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:40,758 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:40,759 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:40,760 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a50a24b8-b322-45b5-a60a-f8e32f8daba2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-099.smt2
[2025-04-28 21:21:40,761 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:40,767 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:40,912 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a50a24b8-b322-45b5-a60a-f8e32f8daba2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-099.smt2
[2025-04-28 21:21:40,916 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:40,918 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:40,919 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:40,919 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:40,919 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:40,922 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,947 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40 Unit
[2025-04-28 21:21:40,947 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:40,949 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:40,950 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:40,950 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:40,967 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,967 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,996 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,998 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:41,001 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:41,002 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:41,004 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:41,005 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:41,006 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:41,022 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,024 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:41,025 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:41,025 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:41,026 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:41,029 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,046 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,057 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:41,060 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:41,069 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:41,069 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:41,069 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:41,070 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure itp given in one single declaration
[2025-04-28 21:21:41,070 INFO  L130     BoogieDeclarations]: Found specification of procedure itp
[2025-04-28 21:21:41,070 INFO  L138     BoogieDeclarations]: Found implementation of procedure itp
[2025-04-28 21:21:41,070 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:41,070 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:41,070 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:41,107 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:41,110 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:41,193 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:41,194 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:41,207 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:41,207 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:41,208 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41 BoogieIcfgContainer
[2025-04-28 21:21:41,208 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:41,212 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:41,213 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:41,217 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:41,217 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/3) ...
[2025-04-28 21:21:41,218 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@172732f2 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,218 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (2/3) ...
[2025-04-28 21:21:41,220 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@172732f2 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,220 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41" (3/3) ...
[2025-04-28 21:21:41,221 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:41,239 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:41,246 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:41,301 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:41,314 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;@41969bb4, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:41,315 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:41,319 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:41,327 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:41,327 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,327 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,328 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,334 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,334 INFO  L85        PathProgramCache]: Analyzing trace with hash -1672547219, now seen corresponding path program 1 times
[2025-04-28 21:21:41,343 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,343 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [42790928]
[2025-04-28 21:21:41,343 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,344 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,373 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:41,394 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:41,394 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,394 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,583 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:41,583 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,584 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [42790928]
[2025-04-28 21:21:41,584 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [42790928] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,585 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,588 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:41,590 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1537791209]
[2025-04-28 21:21:41,592 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,600 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:41,600 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,630 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:41,630 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:41,632 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:41,672 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,673 INFO  L93              Difference]: Finished difference Result 13 states and 14 transitions.
[2025-04-28 21:21:41,674 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:41,676 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:41,678 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,684 INFO  L225             Difference]: With dead ends: 13
[2025-04-28 21:21:41,685 INFO  L226             Difference]: Without dead ends: 13
[2025-04-28 21:21:41,686 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:41,691 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:41,692 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:41,707 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 13 states.
[2025-04-28 21:21:41,737 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 13 to 13.
[2025-04-28 21:21:41,741 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:41,744 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 13 states to 13 states and 14 transitions.
[2025-04-28 21:21:41,745 INFO  L79                 Accepts]: Start accepts. Automaton has 13 states and 14 transitions. Word has length 9
[2025-04-28 21:21:41,746 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,746 INFO  L485      AbstractCegarLoop]: Abstraction has 13 states and 14 transitions.
[2025-04-28 21:21:41,746 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:41,746 INFO  L278                IsEmpty]: Start isEmpty. Operand 13 states and 14 transitions.
[2025-04-28 21:21:41,748 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:41,748 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,748 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,748 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:41,749 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,749 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,750 INFO  L85        PathProgramCache]: Analyzing trace with hash 13498287, now seen corresponding path program 1 times
[2025-04-28 21:21:41,750 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,750 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1854703589]
[2025-04-28 21:21:41,750 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,750 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,761 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:41,778 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:41,782 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,782 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,056 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:42,057 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,057 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1854703589]
[2025-04-28 21:21:42,057 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1854703589] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,057 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [595003577]
[2025-04-28 21:21:42,057 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,060 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,062 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,071 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:42,077 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,146 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:42,163 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:42,163 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,163 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,166 INFO  L256         TraceCheckSpWp]: Trace formula consists of 40 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,172 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,599 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:42,599 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,244 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:43,244 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [595003577] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,244 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,244 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:43,245 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1875816851]
[2025-04-28 21:21:43,245 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,246 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:43,246 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,247 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:43,247 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=22, Invalid=68, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:43,247 INFO  L87              Difference]: Start difference. First operand 13 states and 14 transitions. Second operand  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:43,341 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,341 INFO  L93              Difference]: Finished difference Result 15 states and 16 transitions.
[2025-04-28 21:21:43,342 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:43,343 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7) Word has length 13
[2025-04-28 21:21:43,343 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,344 INFO  L225             Difference]: With dead ends: 15
[2025-04-28 21:21:43,344 INFO  L226             Difference]: Without dead ends: 15
[2025-04-28 21:21:43,344 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 22 SyntacticMatches, 1 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=28, Invalid=82, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:43,345 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 4 mSDsluCounter, 41 mSDsCounter, 0 mSdLazyCounter, 31 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 52 SdHoareTripleChecker+Invalid, 33 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 31 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,345 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 52 Invalid, 33 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 31 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:43,349 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15 states.
[2025-04-28 21:21:43,351 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15 to 15.
[2025-04-28 21:21:43,351 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:43,352 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 15 states to 15 states and 16 transitions.
[2025-04-28 21:21:43,353 INFO  L79                 Accepts]: Start accepts. Automaton has 15 states and 16 transitions. Word has length 13
[2025-04-28 21:21:43,353 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,353 INFO  L485      AbstractCegarLoop]: Abstraction has 15 states and 16 transitions.
[2025-04-28 21:21:43,353 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:43,353 INFO  L278                IsEmpty]: Start isEmpty. Operand 15 states and 16 transitions.
[2025-04-28 21:21:43,354 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:43,354 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,354 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,358 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:43,558 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:43,558 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,559 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,559 INFO  L85        PathProgramCache]: Analyzing trace with hash -1177266959, now seen corresponding path program 2 times
[2025-04-28 21:21:43,559 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,559 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2057464146]
[2025-04-28 21:21:43,559 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:43,559 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,565 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:43,581 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:43,584 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:43,584 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,722 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:43,723 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,723 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2057464146]
[2025-04-28 21:21:43,723 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2057464146] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,723 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [570920544]
[2025-04-28 21:21:43,723 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:43,723 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,726 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,728 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:43,731 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,767 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:43,782 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:43,782 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:43,783 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,784 INFO  L256         TraceCheckSpWp]: Trace formula consists of 55 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,785 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,031 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:44,032 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,931 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:44,931 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [570920544] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,931 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,932 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 13
[2025-04-28 21:21:44,932 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [97857163]
[2025-04-28 21:21:44,932 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,932 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:44,932 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,933 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:44,933 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=31, Invalid=125, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:44,934 INFO  L87              Difference]: Start difference. First operand 15 states and 16 transitions. Second operand  has 13 states, 8 states have (on average 1.875) internal successors, (15), 12 states have internal predecessors, (15), 6 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (10), 5 states have call predecessors, (10), 6 states have call successors, (10)
[2025-04-28 21:21:45,106 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,107 INFO  L93              Difference]: Finished difference Result 17 states and 18 transitions.
[2025-04-28 21:21:45,108 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:45,108 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 8 states have (on average 1.875) internal successors, (15), 12 states have internal predecessors, (15), 6 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (10), 5 states have call predecessors, (10), 6 states have call successors, (10) Word has length 17
[2025-04-28 21:21:45,110 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,110 INFO  L225             Difference]: With dead ends: 17
[2025-04-28 21:21:45,112 INFO  L226             Difference]: Without dead ends: 17
[2025-04-28 21:21:45,112 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 43 GetRequests, 29 SyntacticMatches, 1 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 23 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=45, Invalid=165, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:45,113 INFO  L437           NwaCegarLoop]: 12 mSDtfsCounter, 5 mSDsluCounter, 69 mSDsCounter, 0 mSdLazyCounter, 62 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 81 SdHoareTripleChecker+Invalid, 63 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 62 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,113 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 81 Invalid, 63 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 62 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,114 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17 states.
[2025-04-28 21:21:45,119 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 17 to 17.
[2025-04-28 21:21:45,120 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:45,121 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 18 transitions.
[2025-04-28 21:21:45,121 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 18 transitions. Word has length 17
[2025-04-28 21:21:45,122 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,122 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 18 transitions.
[2025-04-28 21:21:45,122 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 8 states have (on average 1.875) internal successors, (15), 12 states have internal predecessors, (15), 6 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (10), 5 states have call predecessors, (10), 6 states have call successors, (10)
[2025-04-28 21:21:45,122 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 18 transitions.
[2025-04-28 21:21:45,123 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:45,123 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,123 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,129 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:45,324 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:45,324 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,325 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,325 INFO  L85        PathProgramCache]: Analyzing trace with hash 329141299, now seen corresponding path program 3 times
[2025-04-28 21:21:45,325 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,325 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1075982220]
[2025-04-28 21:21:45,325 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:45,325 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,330 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:45,338 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:45,338 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:45,338 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,584 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:45,584 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,584 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1075982220]
[2025-04-28 21:21:45,584 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1075982220] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,584 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1979032041]
[2025-04-28 21:21:45,584 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:45,584 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,587 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,589 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:45,593 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,636 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:45,650 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:45,651 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:45,651 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,653 INFO  L256         TraceCheckSpWp]: Trace formula consists of 70 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,654 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:45,904 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:45,904 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,081 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:47,082 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1979032041] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,082 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,082 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 10] total 16
[2025-04-28 21:21:47,082 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1714462892]
[2025-04-28 21:21:47,082 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,083 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:47,083 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,085 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:47,085 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=200, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:47,085 INFO  L87              Difference]: Start difference. First operand 17 states and 18 transitions. Second operand  has 16 states, 10 states have (on average 1.8) internal successors, (18), 15 states have internal predecessors, (18), 7 states have call successors, (7), 1 states have call predecessors, (7), 9 states have return successors, (13), 7 states have call predecessors, (13), 7 states have call successors, (13)
[2025-04-28 21:21:47,241 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,242 INFO  L93              Difference]: Finished difference Result 19 states and 20 transitions.
[2025-04-28 21:21:47,243 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:47,243 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 10 states have (on average 1.8) internal successors, (18), 15 states have internal predecessors, (18), 7 states have call successors, (7), 1 states have call predecessors, (7), 9 states have return successors, (13), 7 states have call predecessors, (13), 7 states have call successors, (13) Word has length 21
[2025-04-28 21:21:47,244 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,244 INFO  L225             Difference]: With dead ends: 19
[2025-04-28 21:21:47,245 INFO  L226             Difference]: Without dead ends: 19
[2025-04-28 21:21:47,246 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 35 SyntacticMatches, 2 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 50 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=64, Invalid=278, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:47,247 INFO  L437           NwaCegarLoop]: 13 mSDtfsCounter, 6 mSDsluCounter, 66 mSDsCounter, 0 mSdLazyCounter, 58 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 79 SdHoareTripleChecker+Invalid, 59 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 58 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,249 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 79 Invalid, 59 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 58 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:47,250 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 19 states.
[2025-04-28 21:21:47,254 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 19 to 19.
[2025-04-28 21:21:47,255 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:47,256 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 19 states to 19 states and 20 transitions.
[2025-04-28 21:21:47,256 INFO  L79                 Accepts]: Start accepts. Automaton has 19 states and 20 transitions. Word has length 21
[2025-04-28 21:21:47,256 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,257 INFO  L485      AbstractCegarLoop]: Abstraction has 19 states and 20 transitions.
[2025-04-28 21:21:47,257 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 10 states have (on average 1.8) internal successors, (18), 15 states have internal predecessors, (18), 7 states have call successors, (7), 1 states have call predecessors, (7), 9 states have return successors, (13), 7 states have call predecessors, (13), 7 states have call successors, (13)
[2025-04-28 21:21:47,257 INFO  L278                IsEmpty]: Start isEmpty. Operand 19 states and 20 transitions.
[2025-04-28 21:21:47,258 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:47,258 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,258 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,263 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:47,462 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:47,462 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,463 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,463 INFO  L85        PathProgramCache]: Analyzing trace with hash 1761090933, now seen corresponding path program 4 times
[2025-04-28 21:21:47,463 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,463 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1878664337]
[2025-04-28 21:21:47,463 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:47,463 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,468 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:47,476 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:47,476 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:47,477 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,729 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:47,729 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,729 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1878664337]
[2025-04-28 21:21:47,729 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1878664337] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,729 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1819503904]
[2025-04-28 21:21:47,729 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:47,730 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,732 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,734 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:47,738 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,779 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:47,796 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:47,796 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:47,796 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,797 INFO  L256         TraceCheckSpWp]: Trace formula consists of 85 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,799 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,093 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:48,093 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:49,498 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:49,498 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1819503904] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:49,498 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:49,498 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 12] total 19
[2025-04-28 21:21:49,498 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [794653180]
[2025-04-28 21:21:49,499 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,499 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:49,499 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,501 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:49,501 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=49, Invalid=293, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:49,501 INFO  L87              Difference]: Start difference. First operand 19 states and 20 transitions. Second operand  has 19 states, 12 states have (on average 1.75) internal successors, (21), 18 states have internal predecessors, (21), 8 states have call successors, (8), 1 states have call predecessors, (8), 11 states have return successors, (16), 9 states have call predecessors, (16), 8 states have call successors, (16)
[2025-04-28 21:21:49,732 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,732 INFO  L93              Difference]: Finished difference Result 21 states and 22 transitions.
[2025-04-28 21:21:49,733 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:49,733 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 12 states have (on average 1.75) internal successors, (21), 18 states have internal predecessors, (21), 8 states have call successors, (8), 1 states have call predecessors, (8), 11 states have return successors, (16), 9 states have call predecessors, (16), 8 states have call successors, (16) Word has length 25
[2025-04-28 21:21:49,733 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,734 INFO  L225             Difference]: With dead ends: 21
[2025-04-28 21:21:49,734 INFO  L226             Difference]: Without dead ends: 21
[2025-04-28 21:21:49,734 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 65 GetRequests, 42 SyntacticMatches, 2 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 75 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=85, Invalid=421, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:49,735 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 10 mSDsluCounter, 109 mSDsCounter, 0 mSdLazyCounter, 97 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 123 SdHoareTripleChecker+Invalid, 102 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 97 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,736 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 123 Invalid, 102 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 97 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:49,741 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 21 states.
[2025-04-28 21:21:49,743 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 21 to 21.
[2025-04-28 21:21:49,746 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:49,747 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 21 states to 21 states and 22 transitions.
[2025-04-28 21:21:49,747 INFO  L79                 Accepts]: Start accepts. Automaton has 21 states and 22 transitions. Word has length 25
[2025-04-28 21:21:49,747 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,747 INFO  L485      AbstractCegarLoop]: Abstraction has 21 states and 22 transitions.
[2025-04-28 21:21:49,748 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 12 states have (on average 1.75) internal successors, (21), 18 states have internal predecessors, (21), 8 states have call successors, (8), 1 states have call predecessors, (8), 11 states have return successors, (16), 9 states have call predecessors, (16), 8 states have call successors, (16)
[2025-04-28 21:21:49,748 INFO  L278                IsEmpty]: Start isEmpty. Operand 21 states and 22 transitions.
[2025-04-28 21:21:49,748 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:49,749 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,750 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,756 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:49,950 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:49,950 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,951 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,951 INFO  L85        PathProgramCache]: Analyzing trace with hash 1866336439, now seen corresponding path program 5 times
[2025-04-28 21:21:49,951 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,951 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1428032320]
[2025-04-28 21:21:49,951 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:49,951 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,956 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 29 statements into 6 equivalence classes.
[2025-04-28 21:21:49,964 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:49,964 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:49,964 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,171 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:50,171 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,171 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1428032320]
[2025-04-28 21:21:50,171 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1428032320] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,171 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1863655921]
[2025-04-28 21:21:50,171 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:50,171 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,174 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,176 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:50,179 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,221 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 29 statements into 6 equivalence classes.
[2025-04-28 21:21:50,239 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:50,239 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:50,239 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,241 INFO  L256         TraceCheckSpWp]: Trace formula consists of 100 conjuncts, 27 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,244 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,600 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:50,602 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,397 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:52,398 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1863655921] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,398 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,398 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 14] total 22
[2025-04-28 21:21:52,398 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [567952597]
[2025-04-28 21:21:52,398 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,399 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:52,400 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,400 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:52,401 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=404, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:52,401 INFO  L87              Difference]: Start difference. First operand 21 states and 22 transitions. Second operand  has 22 states, 14 states have (on average 1.7142857142857142) internal successors, (24), 21 states have internal predecessors, (24), 9 states have call successors, (9), 1 states have call predecessors, (9), 13 states have return successors, (19), 11 states have call predecessors, (19), 9 states have call successors, (19)
[2025-04-28 21:21:52,682 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,682 INFO  L93              Difference]: Finished difference Result 23 states and 24 transitions.
[2025-04-28 21:21:52,683 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:52,683 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 14 states have (on average 1.7142857142857142) internal successors, (24), 21 states have internal predecessors, (24), 9 states have call successors, (9), 1 states have call predecessors, (9), 13 states have return successors, (19), 11 states have call predecessors, (19), 9 states have call successors, (19) Word has length 29
[2025-04-28 21:21:52,683 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,684 INFO  L225             Difference]: With dead ends: 23
[2025-04-28 21:21:52,684 INFO  L226             Difference]: Without dead ends: 23
[2025-04-28 21:21:52,684 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 76 GetRequests, 48 SyntacticMatches, 3 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 125 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=108, Invalid=594, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:52,685 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 12 mSDsluCounter, 138 mSDsCounter, 0 mSdLazyCounter, 127 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 153 SdHoareTripleChecker+Invalid, 133 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 127 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,685 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 153 Invalid, 133 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 127 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:52,686 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 23 states.
[2025-04-28 21:21:52,689 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 23 to 23.
[2025-04-28 21:21:52,689 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:52,690 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 23 states to 23 states and 24 transitions.
[2025-04-28 21:21:52,690 INFO  L79                 Accepts]: Start accepts. Automaton has 23 states and 24 transitions. Word has length 29
[2025-04-28 21:21:52,690 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,690 INFO  L485      AbstractCegarLoop]: Abstraction has 23 states and 24 transitions.
[2025-04-28 21:21:52,690 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 14 states have (on average 1.7142857142857142) internal successors, (24), 21 states have internal predecessors, (24), 9 states have call successors, (9), 1 states have call predecessors, (9), 13 states have return successors, (19), 11 states have call predecessors, (19), 9 states have call successors, (19)
[2025-04-28 21:21:52,690 INFO  L278                IsEmpty]: Start isEmpty. Operand 23 states and 24 transitions.
[2025-04-28 21:21:52,691 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:52,691 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,691 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,697 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:52,895 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:52,895 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,896 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,896 INFO  L85        PathProgramCache]: Analyzing trace with hash -2107879943, now seen corresponding path program 6 times
[2025-04-28 21:21:52,896 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,896 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1799246349]
[2025-04-28 21:21:52,896 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:52,896 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,901 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:52,911 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:52,911 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:52,911 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,240 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:53,241 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,241 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1799246349]
[2025-04-28 21:21:53,241 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1799246349] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,241 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [741912741]
[2025-04-28 21:21:53,241 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:53,241 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,244 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,246 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:53,249 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,295 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:53,315 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:53,315 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:53,315 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,316 INFO  L256         TraceCheckSpWp]: Trace formula consists of 115 conjuncts, 31 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,318 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,693 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:53,693 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:55,717 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:55,717 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [741912741] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:55,717 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:55,717 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 16] total 25
[2025-04-28 21:21:55,717 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1582195269]
[2025-04-28 21:21:55,717 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,718 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:21:55,718 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,719 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:21:55,719 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=67, Invalid=533, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:55,719 INFO  L87              Difference]: Start difference. First operand 23 states and 24 transitions. Second operand  has 25 states, 16 states have (on average 1.6875) internal successors, (27), 24 states have internal predecessors, (27), 10 states have call successors, (10), 1 states have call predecessors, (10), 15 states have return successors, (22), 13 states have call predecessors, (22), 10 states have call successors, (22)
[2025-04-28 21:21:56,038 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,038 INFO  L93              Difference]: Finished difference Result 25 states and 26 transitions.
[2025-04-28 21:21:56,039 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:56,039 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 16 states have (on average 1.6875) internal successors, (27), 24 states have internal predecessors, (27), 10 states have call successors, (10), 1 states have call predecessors, (10), 15 states have return successors, (22), 13 states have call predecessors, (22), 10 states have call successors, (22) Word has length 33
[2025-04-28 21:21:56,040 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,040 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:21:56,040 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:21:56,041 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 87 GetRequests, 53 SyntacticMatches, 5 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 191 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=133, Invalid=797, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:21:56,042 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 38 mSDsluCounter, 188 mSDsCounter, 0 mSdLazyCounter, 176 mSolverCounterSat, 35 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 47 SdHoareTripleChecker+Valid, 204 SdHoareTripleChecker+Invalid, 211 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 35 IncrementalHoareTripleChecker+Valid, 176 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,042 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [47 Valid, 204 Invalid, 211 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [35 Valid, 176 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:56,042 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:21:56,045 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 25.
[2025-04-28 21:21:56,046 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:56,046 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 26 transitions.
[2025-04-28 21:21:56,046 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 26 transitions. Word has length 33
[2025-04-28 21:21:56,047 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,047 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 26 transitions.
[2025-04-28 21:21:56,047 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 16 states have (on average 1.6875) internal successors, (27), 24 states have internal predecessors, (27), 10 states have call successors, (10), 1 states have call predecessors, (10), 15 states have return successors, (22), 13 states have call predecessors, (22), 10 states have call successors, (22)
[2025-04-28 21:21:56,047 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 26 transitions.
[2025-04-28 21:21:56,048 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:56,048 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,048 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,052 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:56,250 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:56,250 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,250 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,251 INFO  L85        PathProgramCache]: Analyzing trace with hash -254857925, now seen corresponding path program 7 times
[2025-04-28 21:21:56,251 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,251 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1157188387]
[2025-04-28 21:21:56,251 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:56,251 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,255 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:56,264 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:56,264 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,264 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,548 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:56,548 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,548 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1157188387]
[2025-04-28 21:21:56,549 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1157188387] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,549 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [794986555]
[2025-04-28 21:21:56,549 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:56,549 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,552 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,554 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:56,558 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,612 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:56,636 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:56,636 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,636 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,637 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 35 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,639 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,022 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:57,022 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,235 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:59,235 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [794986555] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,235 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,235 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 18] total 28
[2025-04-28 21:21:59,235 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1810659101]
[2025-04-28 21:21:59,236 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,236 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 28 states
[2025-04-28 21:21:59,236 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,237 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 28 interpolants.
[2025-04-28 21:21:59,237 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=76, Invalid=680, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:59,237 INFO  L87              Difference]: Start difference. First operand 25 states and 26 transitions. Second operand  has 28 states, 18 states have (on average 1.6666666666666667) internal successors, (30), 27 states have internal predecessors, (30), 11 states have call successors, (11), 1 states have call predecessors, (11), 17 states have return successors, (25), 15 states have call predecessors, (25), 11 states have call successors, (25)
[2025-04-28 21:21:59,571 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,571 INFO  L93              Difference]: Finished difference Result 27 states and 28 transitions.
[2025-04-28 21:21:59,572 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:59,572 INFO  L79                 Accepts]: Start accepts. Automaton has  has 28 states, 18 states have (on average 1.6666666666666667) internal successors, (30), 27 states have internal predecessors, (30), 11 states have call successors, (11), 1 states have call predecessors, (11), 17 states have return successors, (25), 15 states have call predecessors, (25), 11 states have call successors, (25) Word has length 37
[2025-04-28 21:21:59,573 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,573 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:59,573 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:59,574 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 98 GetRequests, 61 SyntacticMatches, 4 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 228 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=160, Invalid=1030, Unknown=0, NotChecked=0, Total=1190
[2025-04-28 21:21:59,574 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 31 mSDsluCounter, 194 mSDsCounter, 0 mSdLazyCounter, 186 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 41 SdHoareTripleChecker+Valid, 211 SdHoareTripleChecker+Invalid, 211 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 186 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,575 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [41 Valid, 211 Invalid, 211 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 186 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:59,575 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:59,578 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:59,578 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:59,579 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 28 transitions.
[2025-04-28 21:21:59,579 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 28 transitions. Word has length 37
[2025-04-28 21:21:59,579 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,579 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 28 transitions.
[2025-04-28 21:21:59,579 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 28 states, 18 states have (on average 1.6666666666666667) internal successors, (30), 27 states have internal predecessors, (30), 11 states have call successors, (11), 1 states have call predecessors, (11), 17 states have return successors, (25), 15 states have call predecessors, (25), 11 states have call successors, (25)
[2025-04-28 21:21:59,579 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 28 transitions.
[2025-04-28 21:21:59,580 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:59,580 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,581 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,587 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:59,781 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:59,781 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,782 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,782 INFO  L85        PathProgramCache]: Analyzing trace with hash 1201858173, now seen corresponding path program 8 times
[2025-04-28 21:21:59,782 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,782 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [957406676]
[2025-04-28 21:21:59,782 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:59,782 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,786 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 41 statements into 2 equivalence classes.
[2025-04-28 21:21:59,794 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:59,794 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:59,794 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,103 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:22:00,103 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,103 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [957406676]
[2025-04-28 21:22:00,103 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [957406676] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,103 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [491189075]
[2025-04-28 21:22:00,103 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:00,103 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,106 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,108 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:22:00,112 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,177 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 41 statements into 2 equivalence classes.
[2025-04-28 21:22:00,195 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:22:00,195 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:00,195 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,197 INFO  L256         TraceCheckSpWp]: Trace formula consists of 145 conjuncts, 39 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,199 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,613 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:22:00,613 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:03,384 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 100 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:22:03,384 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [491189075] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:03,384 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:03,384 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 20] total 31
[2025-04-28 21:22:03,384 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [914459804]
[2025-04-28 21:22:03,384 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,385 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 31 states
[2025-04-28 21:22:03,385 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,385 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 31 interpolants.
[2025-04-28 21:22:03,386 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=85, Invalid=845, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:22:03,386 INFO  L87              Difference]: Start difference. First operand 27 states and 28 transitions. Second operand  has 31 states, 20 states have (on average 1.65) internal successors, (33), 30 states have internal predecessors, (33), 12 states have call successors, (12), 1 states have call predecessors, (12), 19 states have return successors, (28), 17 states have call predecessors, (28), 12 states have call successors, (28)
[2025-04-28 21:22:03,808 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,808 INFO  L93              Difference]: Finished difference Result 29 states and 30 transitions.
[2025-04-28 21:22:03,808 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:03,809 INFO  L79                 Accepts]: Start accepts. Automaton has  has 31 states, 20 states have (on average 1.65) internal successors, (33), 30 states have internal predecessors, (33), 12 states have call successors, (12), 1 states have call predecessors, (12), 19 states have return successors, (28), 17 states have call predecessors, (28), 12 states have call successors, (28) Word has length 41
[2025-04-28 21:22:03,809 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,809 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:22:03,810 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:22:03,810 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 109 GetRequests, 67 SyntacticMatches, 5 SemanticMatches, 37 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 304 ImplicationChecksByTransitivity, 1.1s TimeCoverageRelationStatistics Valid=189, Invalid=1293, Unknown=0, NotChecked=0, Total=1482
[2025-04-28 21:22:03,811 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 67 mSDsluCounter, 233 mSDsCounter, 0 mSdLazyCounter, 226 mSolverCounterSat, 64 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 78 SdHoareTripleChecker+Valid, 251 SdHoareTripleChecker+Invalid, 290 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 64 IncrementalHoareTripleChecker+Valid, 226 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,811 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [78 Valid, 251 Invalid, 290 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [64 Valid, 226 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:03,812 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:22:03,814 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:22:03,815 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:22:03,815 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 30 transitions.
[2025-04-28 21:22:03,816 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 30 transitions. Word has length 41
[2025-04-28 21:22:03,816 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:03,816 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 30 transitions.
[2025-04-28 21:22:03,816 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 31 states, 20 states have (on average 1.65) internal successors, (33), 30 states have internal predecessors, (33), 12 states have call successors, (12), 1 states have call predecessors, (12), 19 states have return successors, (28), 17 states have call predecessors, (28), 12 states have call successors, (28)
[2025-04-28 21:22:03,816 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 30 transitions.
[2025-04-28 21:22:03,817 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:22:03,817 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:03,817 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:03,822 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:04,018 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:04,018 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,018 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,019 INFO  L85        PathProgramCache]: Analyzing trace with hash -1636582977, now seen corresponding path program 9 times
[2025-04-28 21:22:04,019 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,019 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1426827823]
[2025-04-28 21:22:04,019 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:04,019 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,023 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 45 statements into 10 equivalence classes.
[2025-04-28 21:22:04,035 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:22:04,035 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:22:04,035 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,352 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:22:04,352 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,352 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1426827823]
[2025-04-28 21:22:04,352 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1426827823] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:04,352 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [752694181]
[2025-04-28 21:22:04,352 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:04,352 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,354 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:04,359 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:04,363 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:04,438 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 45 statements into 10 equivalence classes.
[2025-04-28 21:22:04,466 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:22:04,466 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:22:04,466 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,468 INFO  L256         TraceCheckSpWp]: Trace formula consists of 160 conjuncts, 43 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:04,470 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:05,038 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:22:05,038 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:08,412 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:22:08,412 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [752694181] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,412 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,412 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 22] total 34
[2025-04-28 21:22:08,412 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2127537314]
[2025-04-28 21:22:08,412 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,413 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 34 states
[2025-04-28 21:22:08,413 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,414 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 34 interpolants.
[2025-04-28 21:22:08,414 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=94, Invalid=1028, Unknown=0, NotChecked=0, Total=1122
[2025-04-28 21:22:08,414 INFO  L87              Difference]: Start difference. First operand 29 states and 30 transitions. Second operand  has 34 states, 22 states have (on average 1.6363636363636365) internal successors, (36), 33 states have internal predecessors, (36), 13 states have call successors, (13), 1 states have call predecessors, (13), 21 states have return successors, (31), 19 states have call predecessors, (31), 13 states have call successors, (31)
[2025-04-28 21:22:08,945 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:08,945 INFO  L93              Difference]: Finished difference Result 31 states and 32 transitions.
[2025-04-28 21:22:08,946 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:22:08,946 INFO  L79                 Accepts]: Start accepts. Automaton has  has 34 states, 22 states have (on average 1.6363636363636365) internal successors, (36), 33 states have internal predecessors, (36), 13 states have call successors, (13), 1 states have call predecessors, (13), 21 states have return successors, (31), 19 states have call predecessors, (31), 13 states have call successors, (31) Word has length 45
[2025-04-28 21:22:08,946 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,947 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:22:08,947 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:22:08,947 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 120 GetRequests, 72 SyntacticMatches, 7 SemanticMatches, 41 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 403 ImplicationChecksByTransitivity, 1.4s TimeCoverageRelationStatistics Valid=220, Invalid=1586, Unknown=0, NotChecked=0, Total=1806
[2025-04-28 21:22:08,948 INFO  L437           NwaCegarLoop]: 19 mSDtfsCounter, 74 mSDsluCounter, 304 mSDsCounter, 0 mSdLazyCounter, 289 mSolverCounterSat, 70 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 86 SdHoareTripleChecker+Valid, 323 SdHoareTripleChecker+Invalid, 359 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 70 IncrementalHoareTripleChecker+Valid, 289 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,948 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [86 Valid, 323 Invalid, 359 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [70 Valid, 289 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:08,949 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:22:08,952 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 31.
[2025-04-28 21:22:08,952 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:22:08,952 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 32 transitions.
[2025-04-28 21:22:08,953 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 32 transitions. Word has length 45
[2025-04-28 21:22:08,953 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,953 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 32 transitions.
[2025-04-28 21:22:08,953 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 34 states, 22 states have (on average 1.6363636363636365) internal successors, (36), 33 states have internal predecessors, (36), 13 states have call successors, (13), 1 states have call predecessors, (13), 21 states have return successors, (31), 19 states have call predecessors, (31), 13 states have call successors, (31)
[2025-04-28 21:22:08,953 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 32 transitions.
[2025-04-28 21:22:08,954 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 50
[2025-04-28 21:22:08,954 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,954 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:08,960 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:22:09,158 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable10
[2025-04-28 21:22:09,159 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,159 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,159 INFO  L85        PathProgramCache]: Analyzing trace with hash -479336703, now seen corresponding path program 10 times
[2025-04-28 21:22:09,159 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,160 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1408005942]
[2025-04-28 21:22:09,160 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:09,161 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,167 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 49 statements into 2 equivalence classes.
[2025-04-28 21:22:09,173 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:22:09,174 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:09,174 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,617 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:22:09,617 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:09,617 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1408005942]
[2025-04-28 21:22:09,617 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1408005942] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:09,617 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [959360301]
[2025-04-28 21:22:09,617 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:09,617 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,619 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:09,621 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:09,625 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:09,712 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 49 statements into 2 equivalence classes.
[2025-04-28 21:22:09,738 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:22:09,738 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:09,738 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,740 INFO  L256         TraceCheckSpWp]: Trace formula consists of 175 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:09,742 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:10,418 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:22:10,418 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
