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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:25,817 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:25,883 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_933d9773-92a1-420a-9f9e-83df9f605d17/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:25,888 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:25,888 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:25,911 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:25,912 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:25,912 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:25,913 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:25,913 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:25,913 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:25,913 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:25,914 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:25,914 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:25,914 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:25,914 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:25,914 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:25,914 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:25,915 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:25,915 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:25,915 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:25,915 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:25,915 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:25,915 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:25,916 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:25,916 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:25,917 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:26,304 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:26,316 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:26,319 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:26,322 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:26,323 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:26,325 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_933d9773-92a1-420a-9f9e-83df9f605d17/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-067.smt2
[2025-04-28 21:21:26,329 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:26,333 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:26,537 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_933d9773-92a1-420a-9f9e-83df9f605d17/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-067.smt2
[2025-04-28 21:21:26,540 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:26,544 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:26,545 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:26,546 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:26,546 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:26,550 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,576 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26 Unit
[2025-04-28 21:21:26,576 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:26,579 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:26,579 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:26,580 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:26,597 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,598 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,630 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,631 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,633 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,634 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,637 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,637 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,638 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,652 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:26,653 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:26,653 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:26,653 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:26,654 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,657 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:26,670 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:26,682 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:26,685 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:26,696 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:26,697 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:26,697 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:26,697 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:26,697 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:26,697 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:26,697 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:26,697 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:26,697 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:26,740 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:26,743 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:26,836 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:26,836 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:26,849 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:26,850 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:26,851 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:26 BoogieIcfgContainer
[2025-04-28 21:21:26,851 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:26,855 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:26,855 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:26,860 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:26,861 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:26" (1/3) ...
[2025-04-28 21:21:26,862 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@49665f84 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:26, skipping insertion in model container
[2025-04-28 21:21:26,863 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (2/3) ...
[2025-04-28 21:21:26,864 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@49665f84 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:26, skipping insertion in model container
[2025-04-28 21:21:26,864 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:26" (3/3) ...
[2025-04-28 21:21:26,870 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:26,888 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:26,893 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 13 locations, 17 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:26,948 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:26,972 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;@2720eb0e, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:26,973 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:26,976 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 13 states, 6 states have (on average 1.3333333333333333) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 2 states have return successors, (3), 3 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:26,986 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:26,986 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,986 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,987 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,994 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,995 INFO  L85        PathProgramCache]: Analyzing trace with hash -1672547219, now seen corresponding path program 1 times
[2025-04-28 21:21:27,003 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,003 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1770172887]
[2025-04-28 21:21:27,004 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,004 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,040 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:27,063 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:27,064 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,064 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,174 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:27,174 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,174 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1770172887]
[2025-04-28 21:21:27,175 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1770172887] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,175 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,178 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:27,179 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1939562024]
[2025-04-28 21:21:27,180 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,184 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:27,184 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,217 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:27,217 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:27,219 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:27,258 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,258 INFO  L93              Difference]: Finished difference Result 13 states and 14 transitions.
[2025-04-28 21:21:27,260 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:27,261 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:27,262 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,273 INFO  L225             Difference]: With dead ends: 13
[2025-04-28 21:21:27,273 INFO  L226             Difference]: Without dead ends: 13
[2025-04-28 21:21:27,275 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:27,279 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:27,280 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:27,296 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 13 states.
[2025-04-28 21:21:27,314 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 13 to 13.
[2025-04-28 21:21:27,315 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:27,318 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 13 states to 13 states and 14 transitions.
[2025-04-28 21:21:27,320 INFO  L79                 Accepts]: Start accepts. Automaton has 13 states and 14 transitions. Word has length 9
[2025-04-28 21:21:27,320 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,320 INFO  L485      AbstractCegarLoop]: Abstraction has 13 states and 14 transitions.
[2025-04-28 21:21:27,321 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:27,321 INFO  L278                IsEmpty]: Start isEmpty. Operand 13 states and 14 transitions.
[2025-04-28 21:21:27,322 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:27,323 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,323 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,323 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:27,323 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,324 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,324 INFO  L85        PathProgramCache]: Analyzing trace with hash 13498287, now seen corresponding path program 1 times
[2025-04-28 21:21:27,324 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,325 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1718591246]
[2025-04-28 21:21:27,325 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,325 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,333 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:27,347 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:27,347 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,348 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,504 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:27,504 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,504 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1718591246]
[2025-04-28 21:21:27,504 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1718591246] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,505 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [112439700]
[2025-04-28 21:21:27,505 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,505 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,508 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,510 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:27,518 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:27,551 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:27,567 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:27,567 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,568 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,570 INFO  L256         TraceCheckSpWp]: Trace formula consists of 52 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:27,575 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,708 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:27,708 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:28,064 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:28,065 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [112439700] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:28,065 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:28,065 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:28,066 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [54419829]
[2025-04-28 21:21:28,066 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,068 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:28,068 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,069 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:28,069 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=38, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:28,070 INFO  L87              Difference]: Start difference. First operand 13 states and 14 transitions. Second operand  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:28,203 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,204 INFO  L93              Difference]: Finished difference Result 15 states and 16 transitions.
[2025-04-28 21:21:28,205 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:28,206 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5) Word has length 13
[2025-04-28 21:21:28,206 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,206 INFO  L225             Difference]: With dead ends: 15
[2025-04-28 21:21:28,207 INFO  L226             Difference]: Without dead ends: 15
[2025-04-28 21:21:28,207 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 23 SyntacticMatches, 2 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=49, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:28,209 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 5 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 16 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 32 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 16 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,211 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 32 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 16 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:28,212 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15 states.
[2025-04-28 21:21:28,216 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15 to 15.
[2025-04-28 21:21:28,217 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 15 states, 7 states have (on average 1.1428571428571428) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:28,218 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 15 states to 15 states and 16 transitions.
[2025-04-28 21:21:28,218 INFO  L79                 Accepts]: Start accepts. Automaton has 15 states and 16 transitions. Word has length 13
[2025-04-28 21:21:28,219 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,219 INFO  L485      AbstractCegarLoop]: Abstraction has 15 states and 16 transitions.
[2025-04-28 21:21:28,219 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:28,219 INFO  L278                IsEmpty]: Start isEmpty. Operand 15 states and 16 transitions.
[2025-04-28 21:21:28,220 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:28,220 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,220 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,246 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:28,424 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,424 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,425 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,425 INFO  L85        PathProgramCache]: Analyzing trace with hash -1177266959, now seen corresponding path program 2 times
[2025-04-28 21:21:28,425 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,425 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2004491744]
[2025-04-28 21:21:28,426 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:28,426 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,434 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:28,447 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:28,448 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:28,448 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,611 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:28,612 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,612 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2004491744]
[2025-04-28 21:21:28,612 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2004491744] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,612 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [820512652]
[2025-04-28 21:21:28,612 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:28,612 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,616 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,618 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:28,619 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,657 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:28,683 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:28,684 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:28,684 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,688 INFO  L256         TraceCheckSpWp]: Trace formula consists of 72 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,690 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,747 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:28,747 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:29,329 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:29,330 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [820512652] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:29,331 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:29,331 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 10
[2025-04-28 21:21:29,331 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1554707579]
[2025-04-28 21:21:29,331 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,332 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:29,332 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,334 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:29,334 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:29,334 INFO  L87              Difference]: Start difference. First operand 15 states and 16 transitions. Second operand  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:29,419 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,420 INFO  L93              Difference]: Finished difference Result 17 states and 18 transitions.
[2025-04-28 21:21:29,421 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:29,421 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 17
[2025-04-28 21:21:29,422 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,422 INFO  L225             Difference]: With dead ends: 17
[2025-04-28 21:21:29,422 INFO  L226             Difference]: Without dead ends: 17
[2025-04-28 21:21:29,423 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 43 GetRequests, 30 SyntacticMatches, 3 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=42, Invalid=90, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:29,424 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 8 mSDsluCounter, 22 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 33 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,424 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 33 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:29,425 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17 states.
[2025-04-28 21:21:29,430 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 17 to 17.
[2025-04-28 21:21:29,430 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 17 states, 8 states have (on average 1.125) internal successors, (9), 9 states have internal predecessors, (9), 3 states have call successors, (3), 2 states have call predecessors, (3), 5 states have return successors, (6), 5 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:29,432 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 18 transitions.
[2025-04-28 21:21:29,432 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 18 transitions. Word has length 17
[2025-04-28 21:21:29,432 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,432 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 18 transitions.
[2025-04-28 21:21:29,432 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:29,433 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 18 transitions.
[2025-04-28 21:21:29,433 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:29,434 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,434 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:29,440 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:29,639 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,639 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,640 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,640 INFO  L85        PathProgramCache]: Analyzing trace with hash 329141299, now seen corresponding path program 3 times
[2025-04-28 21:21:29,640 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,640 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [435502913]
[2025-04-28 21:21:29,640 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:29,640 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,646 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:29,676 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:29,676 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:29,676 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,911 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:29,912 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,912 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [435502913]
[2025-04-28 21:21:29,912 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [435502913] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,912 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [216390577]
[2025-04-28 21:21:29,912 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:29,912 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,915 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,917 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:29,921 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,965 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:29,987 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:29,987 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:29,987 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,988 INFO  L256         TraceCheckSpWp]: Trace formula consists of 92 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,990 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,042 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 12 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:30,042 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:30,854 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:30,855 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [216390577] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:30,855 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:30,856 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 10] total 12
[2025-04-28 21:21:30,856 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [611315697]
[2025-04-28 21:21:30,856 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,857 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:30,857 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,859 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:30,860 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=92, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:30,860 INFO  L87              Difference]: Start difference. First operand 17 states and 18 transitions. Second operand  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:30,971 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,973 INFO  L93              Difference]: Finished difference Result 19 states and 20 transitions.
[2025-04-28 21:21:30,973 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:30,974 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9) Word has length 21
[2025-04-28 21:21:30,974 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,975 INFO  L225             Difference]: With dead ends: 19
[2025-04-28 21:21:30,975 INFO  L226             Difference]: Without dead ends: 19
[2025-04-28 21:21:30,975 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 37 SyntacticMatches, 4 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 35 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=67, Invalid=143, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:30,976 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 10 mSDsluCounter, 46 mSDsCounter, 0 mSdLazyCounter, 32 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 57 SdHoareTripleChecker+Invalid, 39 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 32 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,976 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 57 Invalid, 39 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 32 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:30,980 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 19 states.
[2025-04-28 21:21:30,983 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 19 to 19.
[2025-04-28 21:21:30,986 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:30,987 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 19 states to 19 states and 20 transitions.
[2025-04-28 21:21:30,988 INFO  L79                 Accepts]: Start accepts. Automaton has 19 states and 20 transitions. Word has length 21
[2025-04-28 21:21:30,988 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,988 INFO  L485      AbstractCegarLoop]: Abstraction has 19 states and 20 transitions.
[2025-04-28 21:21:30,989 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:30,989 INFO  L278                IsEmpty]: Start isEmpty. Operand 19 states and 20 transitions.
[2025-04-28 21:21:30,989 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:30,991 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,991 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,997 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:31,191 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,192 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,192 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,192 INFO  L85        PathProgramCache]: Analyzing trace with hash 1761090933, now seen corresponding path program 4 times
[2025-04-28 21:21:31,192 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,192 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1128521820]
[2025-04-28 21:21:31,193 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:31,193 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,204 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:31,225 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:31,229 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:31,229 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,664 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 3 proven. 20 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:31,664 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,664 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1128521820]
[2025-04-28 21:21:31,664 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1128521820] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,665 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [863735676]
[2025-04-28 21:21:31,665 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:31,665 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,668 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,670 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:31,674 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,725 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:31,751 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:31,751 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:31,751 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,753 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,755 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,871 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:31,871 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,007 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 26 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:33,007 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [863735676] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,007 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,007 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 12] total 19
[2025-04-28 21:21:33,007 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1812695093]
[2025-04-28 21:21:33,007 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,008 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:33,008 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,009 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:33,009 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=91, Invalid=251, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:33,010 INFO  L87              Difference]: Start difference. First operand 19 states and 20 transitions. Second operand  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (16), 6 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:33,157 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,158 INFO  L93              Difference]: Finished difference Result 23 states and 24 transitions.
[2025-04-28 21:21:33,158 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:33,158 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (16), 6 states have call predecessors, (16), 11 states have call successors, (16) Word has length 25
[2025-04-28 21:21:33,159 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,159 INFO  L225             Difference]: With dead ends: 23
[2025-04-28 21:21:33,159 INFO  L226             Difference]: Without dead ends: 23
[2025-04-28 21:21:33,160 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 39 SyntacticMatches, 5 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 157 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=161, Invalid=391, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:33,161 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 17 mSDsluCounter, 55 mSDsCounter, 0 mSdLazyCounter, 38 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 66 SdHoareTripleChecker+Invalid, 51 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 38 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,161 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 66 Invalid, 51 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 38 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:33,162 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 23 states.
[2025-04-28 21:21:33,165 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 23 to 23.
[2025-04-28 21:21:33,165 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:33,166 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 23 states to 23 states and 24 transitions.
[2025-04-28 21:21:33,166 INFO  L79                 Accepts]: Start accepts. Automaton has 23 states and 24 transitions. Word has length 25
[2025-04-28 21:21:33,166 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,166 INFO  L485      AbstractCegarLoop]: Abstraction has 23 states and 24 transitions.
[2025-04-28 21:21:33,166 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (16), 6 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:33,166 INFO  L278                IsEmpty]: Start isEmpty. Operand 23 states and 24 transitions.
[2025-04-28 21:21:33,167 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:33,168 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,168 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,175 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:33,372 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:21:33,372 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,373 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,373 INFO  L85        PathProgramCache]: Analyzing trace with hash -2107879943, now seen corresponding path program 5 times
[2025-04-28 21:21:33,373 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,373 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1119238337]
[2025-04-28 21:21:33,373 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:33,373 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,394 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:33,493 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:33,493 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:33,494 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,844 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 3 proven. 44 refuted. 0 times theorem prover too weak. 31 trivial. 0 not checked.
[2025-04-28 21:21:33,844 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,844 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1119238337]
[2025-04-28 21:21:33,844 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1119238337] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,844 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [792316545]
[2025-04-28 21:21:33,844 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:33,845 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,848 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,850 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:33,855 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,911 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:34,120 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:34,120 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:34,120 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,122 INFO  L256         TraceCheckSpWp]: Trace formula consists of 152 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,124 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,200 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:34,200 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:36,793 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:36,794 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [792316545] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:36,794 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:36,794 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 16] total 19
[2025-04-28 21:21:36,794 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [700207907]
[2025-04-28 21:21:36,794 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,794 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:36,796 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,797 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:36,797 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=97, Invalid=245, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:36,797 INFO  L87              Difference]: Start difference. First operand 23 states and 24 transitions. Second operand  has 19 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 18 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:36,950 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,950 INFO  L93              Difference]: Finished difference Result 25 states and 26 transitions.
[2025-04-28 21:21:36,951 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:36,951 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 18 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16) Word has length 33
[2025-04-28 21:21:36,951 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,952 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:21:36,952 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:21:36,953 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 87 GetRequests, 57 SyntacticMatches, 7 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 149 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=193, Invalid=407, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:36,954 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 16 mSDsluCounter, 61 mSDsCounter, 0 mSdLazyCounter, 45 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 72 SdHoareTripleChecker+Invalid, 54 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 45 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,954 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 72 Invalid, 54 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 45 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,955 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:21:36,958 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 25.
[2025-04-28 21:21:36,959 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:36,959 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 26 transitions.
[2025-04-28 21:21:36,959 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 26 transitions. Word has length 33
[2025-04-28 21:21:36,960 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,960 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 26 transitions.
[2025-04-28 21:21:36,960 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 18 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:36,960 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 26 transitions.
[2025-04-28 21:21:36,961 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:36,961 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,961 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,965 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:37,162 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:37,162 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,163 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,163 INFO  L85        PathProgramCache]: Analyzing trace with hash -254857925, now seen corresponding path program 6 times
[2025-04-28 21:21:37,163 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,163 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [620521007]
[2025-04-28 21:21:37,163 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:37,163 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,171 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 37 statements into 8 equivalence classes.
[2025-04-28 21:21:37,209 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:37,209 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s)
[2025-04-28 21:21:37,210 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,471 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:37,472 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,472 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [620521007]
[2025-04-28 21:21:37,472 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [620521007] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,472 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1534825020]
[2025-04-28 21:21:37,472 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:37,472 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,474 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,476 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:37,481 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,551 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 37 statements into 8 equivalence classes.
[2025-04-28 21:21:37,623 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:37,623 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s)
[2025-04-28 21:21:37,623 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,625 INFO  L256         TraceCheckSpWp]: Trace formula consists of 172 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,626 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,692 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:37,693 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,755 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 77 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:21:40,755 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1534825020] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,755 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,755 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 18] total 20
[2025-04-28 21:21:40,756 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [549709621]
[2025-04-28 21:21:40,756 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,756 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:40,756 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,757 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:40,757 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=108, Invalid=272, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:40,758 INFO  L87              Difference]: Start difference. First operand 25 states and 26 transitions. Second operand  has 20 states, 10 states have (on average 2.1) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:40,905 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,905 INFO  L93              Difference]: Finished difference Result 27 states and 28 transitions.
[2025-04-28 21:21:40,906 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:40,906 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.1) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17) Word has length 37
[2025-04-28 21:21:40,907 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,907 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:40,908 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:40,908 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 98 GetRequests, 65 SyntacticMatches, 8 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 163 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=227, Invalid=475, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:40,909 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 11 mSDsluCounter, 60 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 71 SdHoareTripleChecker+Invalid, 46 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,909 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 71 Invalid, 46 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:40,910 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:40,913 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:40,914 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 3 states have call successors, (3), 2 states have call predecessors, (3), 10 states have return successors, (11), 10 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:40,914 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 28 transitions.
[2025-04-28 21:21:40,914 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 28 transitions. Word has length 37
[2025-04-28 21:21:40,915 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,915 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 28 transitions.
[2025-04-28 21:21:40,915 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.1) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:40,915 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 28 transitions.
[2025-04-28 21:21:40,916 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:40,916 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,916 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,922 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:41,117 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:41,117 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,117 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,117 INFO  L85        PathProgramCache]: Analyzing trace with hash 1201858173, now seen corresponding path program 7 times
[2025-04-28 21:21:41,117 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,117 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [273669368]
[2025-04-28 21:21:41,117 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:41,118 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,124 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-04-28 21:21:41,137 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:41,137 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,137 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,491 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 64 trivial. 0 not checked.
[2025-04-28 21:21:41,491 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,491 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [273669368]
[2025-04-28 21:21:41,491 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [273669368] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,491 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [559554751]
[2025-04-28 21:21:41,491 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:41,492 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,494 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,497 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:41,501 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,627 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 41 statements into 1 equivalence classes.
[2025-04-28 21:21:41,669 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:41,669 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,669 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,671 INFO  L256         TraceCheckSpWp]: Trace formula consists of 192 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,673 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,768 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 64 trivial. 0 not checked.
[2025-04-28 21:21:41,769 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,076 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 100 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:46,076 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [559554751] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,076 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,076 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 20] total 22
[2025-04-28 21:21:46,076 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [991572390]
[2025-04-28 21:21:46,076 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,077 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:46,077 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,078 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:46,078 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=130, Invalid=332, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:46,078 INFO  L87              Difference]: Start difference. First operand 27 states and 28 transitions. Second operand  has 22 states, 11 states have (on average 2.090909090909091) internal successors, (23), 21 states have internal predecessors, (23), 12 states have call successors, (12), 1 states have call predecessors, (12), 10 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19)
[2025-04-28 21:21:46,228 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,228 INFO  L93              Difference]: Finished difference Result 29 states and 30 transitions.
[2025-04-28 21:21:46,229 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:46,229 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 2.090909090909091) internal successors, (23), 21 states have internal predecessors, (23), 12 states have call successors, (12), 1 states have call predecessors, (12), 10 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19) Word has length 41
[2025-04-28 21:21:46,229 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,230 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:46,230 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:21:46,230 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 109 GetRequests, 72 SyntacticMatches, 9 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 210 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=282, Invalid=588, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:46,231 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 11 mSDsluCounter, 78 mSDsCounter, 0 mSdLazyCounter, 55 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 89 SdHoareTripleChecker+Invalid, 56 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 55 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,231 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 89 Invalid, 56 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 55 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:46,232 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:21:46,235 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:21:46,235 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 14 states have (on average 1.0714285714285714) internal successors, (15), 15 states have internal predecessors, (15), 3 states have call successors, (3), 2 states have call predecessors, (3), 11 states have return successors, (12), 11 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:46,236 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 30 transitions.
[2025-04-28 21:21:46,236 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 30 transitions. Word has length 41
[2025-04-28 21:21:46,236 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,236 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 30 transitions.
[2025-04-28 21:21:46,237 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 2.090909090909091) internal successors, (23), 21 states have internal predecessors, (23), 12 states have call successors, (12), 1 states have call predecessors, (12), 10 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19)
[2025-04-28 21:21:46,237 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 30 transitions.
[2025-04-28 21:21:46,239 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:21:46,240 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,241 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,247 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:46,441 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:46,441 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,442 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,442 INFO  L85        PathProgramCache]: Analyzing trace with hash -1636582977, now seen corresponding path program 8 times
[2025-04-28 21:21:46,442 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,442 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1714582573]
[2025-04-28 21:21:46,442 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,442 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,449 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 45 statements into 2 equivalence classes.
[2025-04-28 21:21:46,460 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:46,460 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:46,460 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,775 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:21:46,776 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,776 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1714582573]
[2025-04-28 21:21:46,776 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1714582573] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,776 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1448415572]
[2025-04-28 21:21:46,776 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,776 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,779 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,781 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:46,785 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,951 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 45 statements into 2 equivalence classes.
[2025-04-28 21:21:46,991 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:21:46,991 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:46,991 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,993 INFO  L256         TraceCheckSpWp]: Trace formula consists of 212 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,995 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,071 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:21:47,071 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,025 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 126 refuted. 0 times theorem prover too weak. 45 trivial. 0 not checked.
[2025-04-28 21:21:53,025 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1448415572] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,026 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,026 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 22] total 24
[2025-04-28 21:21:53,026 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1797765687]
[2025-04-28 21:21:53,026 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,027 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:53,027 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,028 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:53,028 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=154, Invalid=398, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:53,028 INFO  L87              Difference]: Start difference. First operand 29 states and 30 transitions. Second operand  has 24 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 13 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:21:53,254 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,255 INFO  L93              Difference]: Finished difference Result 31 states and 32 transitions.
[2025-04-28 21:21:53,255 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:53,255 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 13 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21) Word has length 45
[2025-04-28 21:21:53,256 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,256 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:53,256 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:53,257 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 120 GetRequests, 79 SyntacticMatches, 10 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 263 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=343, Invalid=713, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:53,258 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 49 mSDsluCounter, 69 mSDsCounter, 0 mSdLazyCounter, 50 mSolverCounterSat, 45 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 61 SdHoareTripleChecker+Valid, 80 SdHoareTripleChecker+Invalid, 95 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 45 IncrementalHoareTripleChecker+Valid, 50 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,258 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [61 Valid, 80 Invalid, 95 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [45 Valid, 50 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:53,259 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:53,262 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 31.
[2025-04-28 21:21:53,263 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 15 states have (on average 1.0666666666666667) internal successors, (16), 16 states have internal predecessors, (16), 3 states have call successors, (3), 2 states have call predecessors, (3), 12 states have return successors, (13), 12 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:53,264 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 32 transitions.
[2025-04-28 21:21:53,264 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 32 transitions. Word has length 45
[2025-04-28 21:21:53,264 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,264 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 32 transitions.
[2025-04-28 21:21:53,265 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 13 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:21:53,265 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 32 transitions.
[2025-04-28 21:21:53,266 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 50
[2025-04-28 21:21:53,266 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,266 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,274 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:53,467 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:21:53,467 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,468 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,468 INFO  L85        PathProgramCache]: Analyzing trace with hash -479336703, now seen corresponding path program 9 times
[2025-04-28 21:21:53,468 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,468 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1758700831]
[2025-04-28 21:21:53,468 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:53,469 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,478 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 49 statements into 11 equivalence classes.
[2025-04-28 21:21:53,568 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 11 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:21:53,569 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 11 check-sat command(s)
[2025-04-28 21:21:53,569 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,975 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:21:53,975 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,975 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1758700831]
[2025-04-28 21:21:53,975 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1758700831] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,975 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1666963123]
[2025-04-28 21:21:53,975 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:53,976 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,978 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,980 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:53,984 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,231 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 49 statements into 11 equivalence classes.
[2025-04-28 21:21:54,433 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 11 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:21:54,433 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 11 check-sat command(s)
[2025-04-28 21:21:54,433 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,435 INFO  L256         TraceCheckSpWp]: Trace formula consists of 232 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,439 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,519 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:21:54,520 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
