./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-226.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:44,991 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:45,084 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c660d105-3c1b-4079-b210-cc183ec1455d/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:45,089 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:45,090 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:45,124 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:45,125 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:45,125 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:45,126 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:45,127 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:45,128 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:45,128 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:45,129 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:45,130 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:45,130 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:45,130 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:45,130 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:45,130 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:45,130 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:45,130 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:45,130 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:45,131 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:45,131 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:45,131 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:45,131 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:45,132 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:45,132 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:45,472 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:45,484 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:45,488 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:45,491 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:45,492 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:45,494 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c660d105-3c1b-4079-b210-cc183ec1455d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-226.smt2
[2025-04-28 21:21:45,498 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:45,505 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:45,712 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c660d105-3c1b-4079-b210-cc183ec1455d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-226.smt2
[2025-04-28 21:21:45,716 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:45,720 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:45,721 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:45,721 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:45,721 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:45,726 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,751 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45 Unit
[2025-04-28 21:21:45,751 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:45,752 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:45,752 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:45,753 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:45,767 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,767 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,798 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,798 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,800 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,802 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,804 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,805 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,805 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,815 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:45,816 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:45,816 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:45,817 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:45,818 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (1/1) ...
[2025-04-28 21:21:45,821 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:45,833 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,848 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:45,855 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,866 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:45,867 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:45,867 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:45,867 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fail given in one single declaration
[2025-04-28 21:21:45,867 INFO  L130     BoogieDeclarations]: Found specification of procedure fail
[2025-04-28 21:21:45,867 INFO  L138     BoogieDeclarations]: Found implementation of procedure fail
[2025-04-28 21:21:45,867 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:45,867 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:45,867 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:45,867 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:45,868 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:45,868 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:45,916 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:45,918 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:46,007 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:46,007 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:46,024 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:46,026 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:46,026 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:46 BoogieIcfgContainer
[2025-04-28 21:21:46,026 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:46,031 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:46,031 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:46,037 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:46,038 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:45" (1/3) ...
[2025-04-28 21:21:46,038 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7a4b5477 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:46, skipping insertion in model container
[2025-04-28 21:21:46,039 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:45" (2/3) ...
[2025-04-28 21:21:46,039 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7a4b5477 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:46, skipping insertion in model container
[2025-04-28 21:21:46,039 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:46" (3/3) ...
[2025-04-28 21:21:46,042 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:46,063 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:46,069 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 16 locations, 21 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:46,138 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:46,166 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;@71191bf0, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:46,166 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:46,174 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:46,190 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:46,190 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,191 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,192 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,200 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,201 INFO  L85        PathProgramCache]: Analyzing trace with hash 812378868, now seen corresponding path program 1 times
[2025-04-28 21:21:46,212 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,213 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1413995765]
[2025-04-28 21:21:46,214 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,215 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,255 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:46,273 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:46,274 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,274 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,385 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:46,385 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,386 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1413995765]
[2025-04-28 21:21:46,386 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1413995765] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,387 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,390 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:46,392 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1362867011]
[2025-04-28 21:21:46,393 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,398 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:46,398 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,435 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:46,436 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,438 INFO  L87              Difference]: Start difference. First operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:46,485 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,486 INFO  L93              Difference]: Finished difference Result 16 states and 17 transitions.
[2025-04-28 21:21:46,490 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:46,494 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:46,495 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,506 INFO  L225             Difference]: With dead ends: 16
[2025-04-28 21:21:46,509 INFO  L226             Difference]: Without dead ends: 16
[2025-04-28 21:21:46,515 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,520 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 1 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 35 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,522 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 35 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:46,540 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 16 states.
[2025-04-28 21:21:46,556 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 16 to 16.
[2025-04-28 21:21:46,558 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 16 states, 7 states have (on average 1.1428571428571428) internal successors, (8), 8 states have internal predecessors, (8), 4 states have call successors, (4), 3 states have call predecessors, (4), 4 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:46,561 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 16 states to 16 states and 17 transitions.
[2025-04-28 21:21:46,563 INFO  L79                 Accepts]: Start accepts. Automaton has 16 states and 17 transitions. Word has length 12
[2025-04-28 21:21:46,563 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,564 INFO  L485      AbstractCegarLoop]: Abstraction has 16 states and 17 transitions.
[2025-04-28 21:21:46,564 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:46,564 INFO  L278                IsEmpty]: Start isEmpty. Operand 16 states and 17 transitions.
[2025-04-28 21:21:46,565 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:46,566 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,566 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,566 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:46,566 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,567 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,567 INFO  L85        PathProgramCache]: Analyzing trace with hash 1337627512, now seen corresponding path program 1 times
[2025-04-28 21:21:46,568 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,568 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [352150525]
[2025-04-28 21:21:46,568 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,568 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,575 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:46,592 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:46,592 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,593 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,751 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:46,751 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,751 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [352150525]
[2025-04-28 21:21:46,751 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [352150525] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,752 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [477122553]
[2025-04-28 21:21:46,752 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,752 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,755 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,758 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:46,761 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,827 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:46,849 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:46,849 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,849 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,851 INFO  L256         TraceCheckSpWp]: Trace formula consists of 40 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,856 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,962 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:46,962 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,420 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:47,421 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [477122553] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,421 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,421 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:47,422 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [14510704]
[2025-04-28 21:21:47,422 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,423 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:47,423 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,424 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:47,424 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=38, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:47,425 INFO  L87              Difference]: Start difference. First operand 16 states and 17 transitions. Second operand  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:47,489 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,490 INFO  L93              Difference]: Finished difference Result 18 states and 19 transitions.
[2025-04-28 21:21:47,490 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:47,491 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6) Word has length 16
[2025-04-28 21:21:47,491 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,491 INFO  L225             Difference]: With dead ends: 18
[2025-04-28 21:21:47,492 INFO  L226             Difference]: Without dead ends: 18
[2025-04-28 21:21:47,492 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 29 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:47,493 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 4 mSDsluCounter, 41 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 55 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,493 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 55 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:47,494 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 18 states.
[2025-04-28 21:21:47,497 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 18 to 18.
[2025-04-28 21:21:47,498 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 18 states, 8 states have (on average 1.125) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 5 states have return successors, (6), 5 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:47,498 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 18 states to 18 states and 19 transitions.
[2025-04-28 21:21:47,498 INFO  L79                 Accepts]: Start accepts. Automaton has 18 states and 19 transitions. Word has length 16
[2025-04-28 21:21:47,499 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,499 INFO  L485      AbstractCegarLoop]: Abstraction has 18 states and 19 transitions.
[2025-04-28 21:21:47,499 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:47,499 INFO  L278                IsEmpty]: Start isEmpty. Operand 18 states and 19 transitions.
[2025-04-28 21:21:47,500 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:47,500 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,500 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,507 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:47,701 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,701 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,702 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,702 INFO  L85        PathProgramCache]: Analyzing trace with hash 1410960252, now seen corresponding path program 2 times
[2025-04-28 21:21:47,702 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,702 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [712452045]
[2025-04-28 21:21:47,702 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,703 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,713 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:47,733 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:47,734 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,734 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,940 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:47,940 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,941 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [712452045]
[2025-04-28 21:21:47,941 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [712452045] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,941 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [514912965]
[2025-04-28 21:21:47,941 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,941 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,945 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,947 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:47,951 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,990 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:48,008 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:48,009 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,009 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,012 INFO  L256         TraceCheckSpWp]: Trace formula consists of 52 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,014 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,072 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:48,073 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,694 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:48,694 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [514912965] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,694 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,694 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 10
[2025-04-28 21:21:48,695 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [243003729]
[2025-04-28 21:21:48,695 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,695 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:48,695 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,696 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:48,696 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:48,697 INFO  L87              Difference]: Start difference. First operand 18 states and 19 transitions. Second operand  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:48,782 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,783 INFO  L93              Difference]: Finished difference Result 20 states and 21 transitions.
[2025-04-28 21:21:48,784 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:48,784 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8) Word has length 20
[2025-04-28 21:21:48,787 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,788 INFO  L225             Difference]: With dead ends: 20
[2025-04-28 21:21:48,788 INFO  L226             Difference]: Without dead ends: 20
[2025-04-28 21:21:48,788 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 36 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:48,789 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 8 mSDsluCounter, 39 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 53 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:48,790 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 53 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:48,794 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 20 states.
[2025-04-28 21:21:48,797 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 20 to 20.
[2025-04-28 21:21:48,800 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 20 states, 9 states have (on average 1.1111111111111112) internal successors, (10), 10 states have internal predecessors, (10), 4 states have call successors, (4), 3 states have call predecessors, (4), 6 states have return successors, (7), 6 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:48,801 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 21 transitions.
[2025-04-28 21:21:48,801 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 21 transitions. Word has length 20
[2025-04-28 21:21:48,801 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,802 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 21 transitions.
[2025-04-28 21:21:48,802 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:48,803 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 21 transitions.
[2025-04-28 21:21:48,804 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:48,804 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,805 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,811 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:49,005 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:49,005 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,006 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,006 INFO  L85        PathProgramCache]: Analyzing trace with hash -1097944320, now seen corresponding path program 3 times
[2025-04-28 21:21:49,006 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,006 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [615079058]
[2025-04-28 21:21:49,006 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:49,006 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,012 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:49,040 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:49,042 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:49,042 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,258 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:49,259 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,259 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [615079058]
[2025-04-28 21:21:49,259 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [615079058] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:49,259 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [738628862]
[2025-04-28 21:21:49,259 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:49,259 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,262 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,265 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:49,269 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,318 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:49,341 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:49,341 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:49,341 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,343 INFO  L256         TraceCheckSpWp]: Trace formula consists of 64 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:49,345 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:49,404 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:49,404 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,403 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:50,403 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [738628862] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,403 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,404 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 10] total 12
[2025-04-28 21:21:50,404 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [986552834]
[2025-04-28 21:21:50,404 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,405 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:50,405 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,405 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:50,406 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=92, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:50,406 INFO  L87              Difference]: Start difference. First operand 20 states and 21 transitions. Second operand  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:50,505 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,506 INFO  L93              Difference]: Finished difference Result 22 states and 23 transitions.
[2025-04-28 21:21:50,507 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:50,508 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10) Word has length 24
[2025-04-28 21:21:50,508 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,508 INFO  L225             Difference]: With dead ends: 22
[2025-04-28 21:21:50,508 INFO  L226             Difference]: Without dead ends: 22
[2025-04-28 21:21:50,509 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 60 GetRequests, 43 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:50,510 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 6 mSDsluCounter, 64 mSDsCounter, 0 mSdLazyCounter, 33 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 78 SdHoareTripleChecker+Invalid, 34 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 33 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,510 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 78 Invalid, 34 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 33 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:50,511 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 22 states.
[2025-04-28 21:21:50,515 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 22 to 22.
[2025-04-28 21:21:50,516 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 10 states have (on average 1.1) internal successors, (11), 11 states have internal predecessors, (11), 4 states have call successors, (4), 3 states have call predecessors, (4), 7 states have return successors, (8), 7 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:50,516 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 23 transitions.
[2025-04-28 21:21:50,517 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 23 transitions. Word has length 24
[2025-04-28 21:21:50,517 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,517 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 23 transitions.
[2025-04-28 21:21:50,519 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:50,520 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 23 transitions.
[2025-04-28 21:21:50,521 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:50,521 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,521 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,527 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:50,725 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,726 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,726 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,726 INFO  L85        PathProgramCache]: Analyzing trace with hash 306702852, now seen corresponding path program 4 times
[2025-04-28 21:21:50,727 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,727 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2108354702]
[2025-04-28 21:21:50,727 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:50,727 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,732 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:50,743 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:50,743 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:50,743 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,954 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 23 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:50,954 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,954 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2108354702]
[2025-04-28 21:21:50,954 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2108354702] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,954 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [203699725]
[2025-04-28 21:21:50,954 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:50,954 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,958 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,960 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:50,963 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:51,001 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:51,016 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:51,017 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:51,017 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,018 INFO  L256         TraceCheckSpWp]: Trace formula consists of 76 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:51,019 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:51,096 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:51,096 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,498 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 26 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:52,498 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [203699725] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,498 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,498 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 12] total 17
[2025-04-28 21:21:52,498 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2076339205]
[2025-04-28 21:21:52,498 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,499 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:52,500 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,501 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:52,502 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=71, Invalid=201, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:52,502 INFO  L87              Difference]: Start difference. First operand 22 states and 23 transitions. Second operand  has 17 states, 8 states have (on average 2.375) internal successors, (19), 16 states have internal predecessors, (19), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (14), 6 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:21:52,744 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,744 INFO  L93              Difference]: Finished difference Result 26 states and 27 transitions.
[2025-04-28 21:21:52,747 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:52,748 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.375) internal successors, (19), 16 states have internal predecessors, (19), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (14), 6 states have call predecessors, (14), 10 states have call successors, (14) Word has length 28
[2025-04-28 21:21:52,748 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,749 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:52,749 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:52,749 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 73 GetRequests, 47 SyntacticMatches, 5 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 89 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=149, Invalid=357, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:52,750 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 13 mSDsluCounter, 97 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 111 SdHoareTripleChecker+Invalid, 59 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 44 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,751 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 111 Invalid, 59 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:52,755 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:52,762 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:52,762 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.0833333333333333) internal successors, (13), 13 states have internal predecessors, (13), 4 states have call successors, (4), 3 states have call predecessors, (4), 9 states have return successors, (10), 9 states have call predecessors, (10), 4 states have call successors, (10)
[2025-04-28 21:21:52,763 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 27 transitions.
[2025-04-28 21:21:52,763 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 27 transitions. Word has length 28
[2025-04-28 21:21:52,763 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,763 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 27 transitions.
[2025-04-28 21:21:52,764 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.375) internal successors, (19), 16 states have internal predecessors, (19), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (14), 6 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:21:52,764 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 27 transitions.
[2025-04-28 21:21:52,766 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:52,767 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,767 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,773 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:52,971 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:52,972 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,972 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,972 INFO  L85        PathProgramCache]: Analyzing trace with hash 822478476, now seen corresponding path program 5 times
[2025-04-28 21:21:52,973 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,973 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [665406031]
[2025-04-28 21:21:52,973 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:52,973 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,980 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:53,015 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:53,015 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:53,015 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,352 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:53,352 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,352 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [665406031]
[2025-04-28 21:21:53,352 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [665406031] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,353 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [840273725]
[2025-04-28 21:21:53,353 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:53,353 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,356 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,359 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:53,363 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,424 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:53,458 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:53,458 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:53,458 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,459 INFO  L256         TraceCheckSpWp]: Trace formula consists of 100 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,461 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,539 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 42 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:53,539 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,312 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:56,313 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [840273725] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,313 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,313 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 16] total 19
[2025-04-28 21:21:56,313 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [398899]
[2025-04-28 21:21:56,313 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,314 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:56,314 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,314 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:56,315 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=97, Invalid=245, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:56,315 INFO  L87              Difference]: Start difference. First operand 26 states and 27 transitions. Second operand  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (17), 7 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:56,468 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,468 INFO  L93              Difference]: Finished difference Result 28 states and 29 transitions.
[2025-04-28 21:21:56,469 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:56,469 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (17), 7 states have call predecessors, (17), 11 states have call successors, (17) Word has length 36
[2025-04-28 21:21:56,469 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,470 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:56,470 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:56,471 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 93 GetRequests, 63 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:56,471 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 20 mSDsluCounter, 76 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 90 SdHoareTripleChecker+Invalid, 54 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,472 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 90 Invalid, 54 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,472 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:56,475 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 28.
[2025-04-28 21:21:56,476 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 4 states have call successors, (4), 3 states have call predecessors, (4), 10 states have return successors, (11), 10 states have call predecessors, (11), 4 states have call successors, (11)
[2025-04-28 21:21:56,476 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 29 transitions.
[2025-04-28 21:21:56,477 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 29 transitions. Word has length 36
[2025-04-28 21:21:56,477 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,477 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 29 transitions.
[2025-04-28 21:21:56,477 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (17), 7 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:56,477 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 29 transitions.
[2025-04-28 21:21:56,478 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:56,478 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,478 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,484 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:56,682 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:56,683 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,683 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,683 INFO  L85        PathProgramCache]: Analyzing trace with hash -1020351472, now seen corresponding path program 6 times
[2025-04-28 21:21:56,683 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,683 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1464112670]
[2025-04-28 21:21:56,683 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:56,684 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,691 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 40 statements into 8 equivalence classes.
[2025-04-28 21:21:56,714 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:56,714 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s)
[2025-04-28 21:21:56,714 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,022 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 56 refuted. 0 times theorem prover too weak. 49 trivial. 0 not checked.
[2025-04-28 21:21:57,022 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,022 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1464112670]
[2025-04-28 21:21:57,022 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1464112670] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,022 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [862020300]
[2025-04-28 21:21:57,022 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:57,022 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,025 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,028 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:57,032 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,115 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 40 statements into 8 equivalence classes.
[2025-04-28 21:21:57,140 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:57,140 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s)
[2025-04-28 21:21:57,141 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,142 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,144 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,203 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 56 refuted. 0 times theorem prover too weak. 49 trivial. 0 not checked.
[2025-04-28 21:21:57,203 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,136 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:22:01,136 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [862020300] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,136 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,137 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 18] total 20
[2025-04-28 21:22:01,137 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1684428608]
[2025-04-28 21:22:01,137 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,138 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:22:01,138 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,139 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:22:01,142 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=108, Invalid=272, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:22:01,142 INFO  L87              Difference]: Start difference. First operand 28 states and 29 transitions. Second operand  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (18), 8 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:22:01,322 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,322 INFO  L93              Difference]: Finished difference Result 30 states and 31 transitions.
[2025-04-28 21:22:01,324 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:22:01,324 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (18), 8 states have call predecessors, (18), 11 states have call successors, (18) Word has length 40
[2025-04-28 21:22:01,324 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,325 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:22:01,325 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:22:01,326 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 104 GetRequests, 71 SyntacticMatches, 8 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 163 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=227, Invalid=475, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:01,327 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 37 mSDsluCounter, 95 mSDsCounter, 0 mSdLazyCounter, 43 mSolverCounterSat, 35 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 47 SdHoareTripleChecker+Valid, 109 SdHoareTripleChecker+Invalid, 78 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 35 IncrementalHoareTripleChecker+Valid, 43 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,329 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [47 Valid, 109 Invalid, 78 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [35 Valid, 43 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:01,330 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:22:01,333 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 30.
[2025-04-28 21:22:01,333 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 30 states, 14 states have (on average 1.0714285714285714) internal successors, (15), 15 states have internal predecessors, (15), 4 states have call successors, (4), 3 states have call predecessors, (4), 11 states have return successors, (12), 11 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:22:01,335 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 31 transitions.
[2025-04-28 21:22:01,336 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 31 transitions. Word has length 40
[2025-04-28 21:22:01,336 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,336 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 31 transitions.
[2025-04-28 21:22:01,336 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (18), 8 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:22:01,336 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 31 transitions.
[2025-04-28 21:22:01,337 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:22:01,337 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,338 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,342 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:01,539 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,539 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,540 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,540 INFO  L85        PathProgramCache]: Analyzing trace with hash 1491263764, now seen corresponding path program 7 times
[2025-04-28 21:22:01,540 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,540 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2040041466]
[2025-04-28 21:22:01,540 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:01,540 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,550 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:22:01,564 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:22:01,564 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,564 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,925 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 64 trivial. 0 not checked.
[2025-04-28 21:22:01,925 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,926 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2040041466]
[2025-04-28 21:22:01,926 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2040041466] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:01,926 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [515984555]
[2025-04-28 21:22:01,926 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:01,926 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,929 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:01,932 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:01,935 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,090 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:22:02,118 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:22:02,118 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:02,118 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,120 INFO  L256         TraceCheckSpWp]: Trace formula consists of 124 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,122 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,223 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 64 trivial. 0 not checked.
[2025-04-28 21:22:02,223 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:07,780 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 100 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:22:07,780 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [515984555] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:07,781 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:07,781 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 20] total 22
[2025-04-28 21:22:07,781 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1173488764]
[2025-04-28 21:22:07,781 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:07,782 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:07,782 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:07,782 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:07,783 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=130, Invalid=332, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:07,783 INFO  L87              Difference]: Start difference. First operand 30 states and 31 transitions. Second operand  has 22 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 21 states have internal predecessors, (24), 12 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 12 states have call successors, (20)
[2025-04-28 21:22:07,952 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,952 INFO  L93              Difference]: Finished difference Result 32 states and 33 transitions.
[2025-04-28 21:22:07,953 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:07,953 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 21 states have internal predecessors, (24), 12 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 12 states have call successors, (20) Word has length 44
[2025-04-28 21:22:07,954 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:07,954 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:22:07,954 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:22:07,955 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 115 GetRequests, 78 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:22:07,956 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 22 mSDsluCounter, 101 mSDsCounter, 0 mSdLazyCounter, 50 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 33 SdHoareTripleChecker+Valid, 115 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 50 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:07,956 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [33 Valid, 115 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 50 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:07,957 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:22:07,960 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:22:07,960 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 15 states have (on average 1.0666666666666667) internal successors, (16), 16 states have internal predecessors, (16), 4 states have call successors, (4), 3 states have call predecessors, (4), 12 states have return successors, (13), 12 states have call predecessors, (13), 4 states have call successors, (13)
[2025-04-28 21:22:07,961 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 33 transitions.
[2025-04-28 21:22:07,961 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 33 transitions. Word has length 44
[2025-04-28 21:22:07,962 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:07,962 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 33 transitions.
[2025-04-28 21:22:07,962 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 21 states have internal predecessors, (24), 12 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 12 states have call successors, (20)
[2025-04-28 21:22:07,962 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 33 transitions.
[2025-04-28 21:22:07,963 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:22:07,963 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:07,963 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:07,970 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:22:08,167 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:22:08,168 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:08,168 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:08,168 INFO  L85        PathProgramCache]: Analyzing trace with hash -635927144, now seen corresponding path program 8 times
[2025-04-28 21:22:08,168 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:08,168 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [115817856]
[2025-04-28 21:22:08,168 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:08,169 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:08,176 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 48 statements into 2 equivalence classes.
[2025-04-28 21:22:08,186 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:22:08,187 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:08,187 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,550 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:22:08,550 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:08,551 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [115817856]
[2025-04-28 21:22:08,551 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [115817856] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:08,551 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [256168238]
[2025-04-28 21:22:08,551 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:08,551 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:08,554 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:08,556 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:08,561 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:22:08,758 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 48 statements into 2 equivalence classes.
[2025-04-28 21:22:08,784 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:22:08,784 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:08,784 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,786 INFO  L256         TraceCheckSpWp]: Trace formula consists of 136 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:08,788 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:08,864 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:22:08,864 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:16,371 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 126 refuted. 0 times theorem prover too weak. 45 trivial. 0 not checked.
[2025-04-28 21:22:16,372 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [256168238] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:16,372 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:16,372 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 22] total 24
[2025-04-28 21:22:16,372 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [687012012]
[2025-04-28 21:22:16,372 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:16,373 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:22:16,373 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:16,374 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:22:16,374 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=154, Invalid=398, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:22:16,375 INFO  L87              Difference]: Start difference. First operand 32 states and 33 transitions. Second operand  has 24 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 23 states have internal predecessors, (26), 13 states have call successors, (14), 1 states have call predecessors, (14), 11 states have return successors, (22), 10 states have call predecessors, (22), 13 states have call successors, (22)
[2025-04-28 21:22:16,569 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:16,569 INFO  L93              Difference]: Finished difference Result 34 states and 35 transitions.
[2025-04-28 21:22:16,573 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:22:16,574 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 23 states have internal predecessors, (26), 13 states have call successors, (14), 1 states have call predecessors, (14), 11 states have return successors, (22), 10 states have call predecessors, (22), 13 states have call successors, (22) Word has length 48
[2025-04-28 21:22:16,574 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:16,575 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:22:16,575 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:22:16,576 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 126 GetRequests, 85 SyntacticMatches, 10 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 263 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=343, Invalid=713, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:16,576 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 32 mSDsluCounter, 113 mSDsCounter, 0 mSdLazyCounter, 52 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 44 SdHoareTripleChecker+Valid, 127 SdHoareTripleChecker+Invalid, 78 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 52 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:16,577 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [44 Valid, 127 Invalid, 78 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 52 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:16,581 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:22:16,585 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 34.
[2025-04-28 21:22:16,585 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 16 states have (on average 1.0625) internal successors, (17), 17 states have internal predecessors, (17), 4 states have call successors, (4), 3 states have call predecessors, (4), 13 states have return successors, (14), 13 states have call predecessors, (14), 4 states have call successors, (14)
[2025-04-28 21:22:16,586 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 35 transitions.
[2025-04-28 21:22:16,586 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 35 transitions. Word has length 48
[2025-04-28 21:22:16,586 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:16,586 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 35 transitions.
[2025-04-28 21:22:16,586 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 23 states have internal predecessors, (26), 13 states have call successors, (14), 1 states have call predecessors, (14), 11 states have return successors, (22), 10 states have call predecessors, (22), 13 states have call successors, (22)
[2025-04-28 21:22:16,586 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 35 transitions.
[2025-04-28 21:22:16,587 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:22:16,587 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:16,588 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:16,593 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:22:16,790 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:16,790 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:16,791 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:16,791 INFO  L85        PathProgramCache]: Analyzing trace with hash -722634340, now seen corresponding path program 9 times
[2025-04-28 21:22:16,791 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:16,791 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [742527860]
[2025-04-28 21:22:16,791 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:16,791 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:16,799 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 52 statements into 11 equivalence classes.
[2025-04-28 21:22:16,822 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 11 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:22:16,822 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 11 check-sat command(s)
[2025-04-28 21:22:16,822 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:17,202 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:22:17,202 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:17,202 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [742527860]
[2025-04-28 21:22:17,202 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [742527860] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:17,202 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1307757618]
[2025-04-28 21:22:17,202 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:17,203 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:17,205 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:17,208 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:17,214 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:17,530 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 52 statements into 11 equivalence classes.
[2025-04-28 21:22:17,572 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 11 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:22:17,572 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 11 check-sat command(s)
[2025-04-28 21:22:17,572 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:17,574 INFO  L256         TraceCheckSpWp]: Trace formula consists of 148 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:17,576 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:17,669 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:22:17,669 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
