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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:16,673 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:16,769 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96b8eb66-06d4-4bf8-824b-ca96ea7b5b20/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:16,776 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:16,777 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:16,810 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:16,811 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:16,812 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:16,812 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:16,813 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:16,814 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:16,815 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:16,815 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:16,815 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:16,815 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:16,816 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:16,816 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:16,816 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:16,816 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:16,816 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:16,817 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:16,817 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:16,817 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:16,817 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:16,817 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:16,818 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:16,818 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:17,141 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:17,153 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:17,156 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:17,157 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:17,160 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:17,161 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96b8eb66-06d4-4bf8-824b-ca96ea7b5b20/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-268.smt2
[2025-04-28 21:21:17,163 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:17,167 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:17,332 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96b8eb66-06d4-4bf8-824b-ca96ea7b5b20/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-268.smt2
[2025-04-28 21:21:17,335 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:17,337 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:17,337 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:17,338 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:17,338 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:17,341 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,362 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17 Unit
[2025-04-28 21:21:17,363 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:17,364 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:17,364 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:17,364 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:17,382 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,383 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,413 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,414 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,416 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,418 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,420 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,420 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,421 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,436 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:17,437 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:17,437 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:17,437 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:17,440 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (1/1) ...
[2025-04-28 21:21:17,443 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:17,458 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:17,469 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:17,472 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:17,481 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:17,482 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:17,482 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:17,482 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fail given in one single declaration
[2025-04-28 21:21:17,482 INFO  L130     BoogieDeclarations]: Found specification of procedure fail
[2025-04-28 21:21:17,482 INFO  L138     BoogieDeclarations]: Found implementation of procedure fail
[2025-04-28 21:21:17,482 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:17,482 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:17,482 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:17,482 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:17,482 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:17,483 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:17,518 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:17,520 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:17,586 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:17,586 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:17,599 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:17,604 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:17,604 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17 BoogieIcfgContainer
[2025-04-28 21:21:17,604 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:17,607 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:17,607 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:17,614 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:17,616 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:17" (1/3) ...
[2025-04-28 21:21:17,617 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5a0754c5 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,617 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:17" (2/3) ...
[2025-04-28 21:21:17,617 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5a0754c5 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,617 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17" (3/3) ...
[2025-04-28 21:21:17,619 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:17,635 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:17,641 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:17,692 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:17,704 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;@2806f3c8, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:17,704 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:17,710 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:17,716 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:17,717 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,717 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,718 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,722 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,723 INFO  L85        PathProgramCache]: Analyzing trace with hash -121084841, now seen corresponding path program 1 times
[2025-04-28 21:21:17,731 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,731 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [47979548]
[2025-04-28 21:21:17,732 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,732 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,766 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:17,783 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:17,784 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,784 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,878 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:17,879 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,881 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [47979548]
[2025-04-28 21:21:17,882 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [47979548] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,882 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,885 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:17,887 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1641167502]
[2025-04-28 21:21:17,889 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,893 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:17,893 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,915 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:17,916 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,917 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:17,954 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,954 INFO  L93              Difference]: Finished difference Result 16 states and 17 transitions.
[2025-04-28 21:21:17,956 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:17,957 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:17,958 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,964 INFO  L225             Difference]: With dead ends: 16
[2025-04-28 21:21:17,964 INFO  L226             Difference]: Without dead ends: 16
[2025-04-28 21:21:17,966 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:17,969 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:17,970 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:17,985 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 16 states.
[2025-04-28 21:21:18,004 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 16 to 16.
[2025-04-28 21:21:18,006 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:18,010 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 16 states to 16 states and 17 transitions.
[2025-04-28 21:21:18,012 INFO  L79                 Accepts]: Start accepts. Automaton has 16 states and 17 transitions. Word has length 12
[2025-04-28 21:21:18,012 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,012 INFO  L485      AbstractCegarLoop]: Abstraction has 16 states and 17 transitions.
[2025-04-28 21:21:18,012 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:18,013 INFO  L278                IsEmpty]: Start isEmpty. Operand 16 states and 17 transitions.
[2025-04-28 21:21:18,014 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:18,014 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,014 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:18,014 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:18,014 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,015 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,015 INFO  L85        PathProgramCache]: Analyzing trace with hash -2109633831, now seen corresponding path program 1 times
[2025-04-28 21:21:18,015 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,015 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1585952462]
[2025-04-28 21:21:18,017 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,017 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,027 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:18,058 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:18,058 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,058 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,225 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:18,225 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,226 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1585952462]
[2025-04-28 21:21:18,226 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1585952462] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:18,226 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1497809166]
[2025-04-28 21:21:18,226 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,226 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:18,229 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:18,231 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:18,235 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:18,310 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:18,330 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:18,331 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,331 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,333 INFO  L256         TraceCheckSpWp]: Trace formula consists of 50 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:18,339 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:18,562 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:18,562 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:18,961 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:18,962 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1497809166] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:18,962 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:18,962 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 12
[2025-04-28 21:21:18,963 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [162901764]
[2025-04-28 21:21:18,963 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,964 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:18,964 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,965 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:18,966 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=107, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:18,967 INFO  L87              Difference]: Start difference. First operand 16 states and 17 transitions. Second operand  has 12 states, 6 states have (on average 2.5) internal successors, (15), 11 states have internal predecessors, (15), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:19,225 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,225 INFO  L93              Difference]: Finished difference Result 26 states and 31 transitions.
[2025-04-28 21:21:19,226 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:19,227 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.5) internal successors, (15), 11 states have internal predecessors, (15), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8) Word has length 16
[2025-04-28 21:21:19,228 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,229 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:19,229 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:19,230 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 43 GetRequests, 25 SyntacticMatches, 2 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 26 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=63, Invalid=243, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:19,232 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 12 mSDsluCounter, 87 mSDsCounter, 0 mSdLazyCounter, 66 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 101 SdHoareTripleChecker+Invalid, 91 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 66 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,233 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 101 Invalid, 91 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 66 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:19,236 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:19,246 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:19,246 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 13 states have internal predecessors, (14), 6 states have call successors, (6), 5 states have call predecessors, (6), 7 states have return successors, (11), 7 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:21:19,248 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 31 transitions.
[2025-04-28 21:21:19,249 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 31 transitions. Word has length 16
[2025-04-28 21:21:19,249 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,249 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 31 transitions.
[2025-04-28 21:21:19,249 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.5) internal successors, (15), 11 states have internal predecessors, (15), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:19,249 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 31 transitions.
[2025-04-28 21:21:19,250 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:19,251 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,251 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:19,258 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:19,456 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:19,456 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,457 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,457 INFO  L85        PathProgramCache]: Analyzing trace with hash -1008473509, now seen corresponding path program 2 times
[2025-04-28 21:21:19,457 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,457 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [46702439]
[2025-04-28 21:21:19,457 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:19,458 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,464 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:19,477 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:19,478 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:19,478 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,661 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:19,661 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,662 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [46702439]
[2025-04-28 21:21:19,662 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [46702439] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:19,662 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [708301413]
[2025-04-28 21:21:19,662 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:19,662 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:19,665 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:19,667 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:19,671 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:19,701 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:19,715 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:19,715 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:19,715 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,716 INFO  L256         TraceCheckSpWp]: Trace formula consists of 66 conjuncts, 12 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:19,718 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:19,967 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:19,967 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:21,367 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:21,368 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [708301413] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:21,368 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:21,368 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 13
[2025-04-28 21:21:21,368 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1557344781]
[2025-04-28 21:21:21,368 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,369 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:21,369 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,371 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:21,371 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=41, Invalid=115, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:21,372 INFO  L87              Difference]: Start difference. First operand 26 states and 31 transitions. Second operand  has 13 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (10), 4 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:21,524 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,528 INFO  L93              Difference]: Finished difference Result 38 states and 43 transitions.
[2025-04-28 21:21:21,528 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:21,529 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (10), 4 states have call predecessors, (10), 8 states have call successors, (10) Word has length 20
[2025-04-28 21:21:21,529 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,529 INFO  L225             Difference]: With dead ends: 38
[2025-04-28 21:21:21,529 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:21,530 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 50 GetRequests, 32 SyntacticMatches, 4 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 50 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=68, Invalid=172, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:21,531 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 9 mSDsluCounter, 67 mSDsCounter, 0 mSdLazyCounter, 31 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 81 SdHoareTripleChecker+Invalid, 37 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 31 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,531 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 81 Invalid, 37 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 31 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:21,536 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:21,540 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 26.
[2025-04-28 21:21:21,542 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 13 states have internal predecessors, (14), 6 states have call successors, (6), 5 states have call predecessors, (6), 7 states have return successors, (8), 7 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:21,542 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 28 transitions.
[2025-04-28 21:21:21,543 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 28 transitions. Word has length 20
[2025-04-28 21:21:21,543 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,543 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 28 transitions.
[2025-04-28 21:21:21,543 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (10), 4 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:21,544 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 28 transitions.
[2025-04-28 21:21:21,545 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:21,545 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,546 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:21,551 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:21,750 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:21,750 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,751 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,751 INFO  L85        PathProgramCache]: Analyzing trace with hash -888646561, now seen corresponding path program 3 times
[2025-04-28 21:21:21,751 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,751 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1902578906]
[2025-04-28 21:21:21,751 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:21,751 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,758 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 28 statements into 5 equivalence classes.
[2025-04-28 21:21:21,776 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 5 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:21,776 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 5 check-sat command(s)
[2025-04-28 21:21:21,776 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,290 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 3 proven. 23 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:22,291 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,291 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1902578906]
[2025-04-28 21:21:22,291 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1902578906] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:22,291 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2123490535]
[2025-04-28 21:21:22,291 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:22,291 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,294 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,296 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:22,300 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:22,342 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 28 statements into 5 equivalence classes.
[2025-04-28 21:21:22,364 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 5 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:22,364 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 5 check-sat command(s)
[2025-04-28 21:21:22,364 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,366 INFO  L256         TraceCheckSpWp]: Trace formula consists of 98 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:22,368 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:22,718 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 3 proven. 22 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:22,718 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:26,351 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:26,351 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2123490535] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:26,351 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:26,351 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 12] total 20
[2025-04-28 21:21:26,351 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [923218987]
[2025-04-28 21:21:26,352 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,352 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:26,352 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,353 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:26,353 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=89, Invalid=291, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:26,353 INFO  L87              Difference]: Start difference. First operand 26 states and 28 transitions. Second operand  has 20 states, 8 states have (on average 2.75) internal successors, (22), 19 states have internal predecessors, (22), 13 states have call successors, (14), 1 states have call predecessors, (14), 7 states have return successors, (16), 6 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:26,536 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,537 INFO  L93              Difference]: Finished difference Result 38 states and 42 transitions.
[2025-04-28 21:21:26,537 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:26,538 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 8 states have (on average 2.75) internal successors, (22), 19 states have internal predecessors, (22), 13 states have call successors, (14), 1 states have call predecessors, (14), 7 states have return successors, (16), 6 states have call predecessors, (16), 13 states have call successors, (16) Word has length 28
[2025-04-28 21:21:26,538 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,540 INFO  L225             Difference]: With dead ends: 38
[2025-04-28 21:21:26,540 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:26,541 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 71 GetRequests, 45 SyntacticMatches, 4 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 119 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=157, Invalid=395, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:26,542 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 11 mSDsluCounter, 105 mSDsCounter, 0 mSdLazyCounter, 50 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 119 SdHoareTripleChecker+Invalid, 56 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 50 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,542 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 119 Invalid, 56 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 50 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:26,544 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:26,549 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 28.
[2025-04-28 21:21:26,549 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 13 states have (on average 1.1538461538461537) internal successors, (15), 14 states have internal predecessors, (15), 6 states have call successors, (6), 5 states have call predecessors, (6), 8 states have return successors, (9), 8 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:21:26,550 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 30 transitions.
[2025-04-28 21:21:26,550 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 30 transitions. Word has length 28
[2025-04-28 21:21:26,551 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,551 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 30 transitions.
[2025-04-28 21:21:26,551 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 8 states have (on average 2.75) internal successors, (22), 19 states have internal predecessors, (22), 13 states have call successors, (14), 1 states have call predecessors, (14), 7 states have return successors, (16), 6 states have call predecessors, (16), 13 states have call successors, (16)
[2025-04-28 21:21:26,551 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 30 transitions.
[2025-04-28 21:21:26,552 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:26,552 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,552 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:26,558 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:26,757 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:26,757 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,758 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,758 INFO  L85        PathProgramCache]: Analyzing trace with hash 1183604449, now seen corresponding path program 4 times
[2025-04-28 21:21:26,758 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,758 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1769384981]
[2025-04-28 21:21:26,758 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:26,758 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,765 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:21:26,778 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:26,778 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:26,778 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,012 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 2 proven. 28 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:27,012 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,013 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1769384981]
[2025-04-28 21:21:27,013 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1769384981] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,013 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1082500394]
[2025-04-28 21:21:27,013 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:27,013 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,016 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,019 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:27,023 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:27,096 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:21:27,116 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:27,116 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:27,117 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,118 INFO  L256         TraceCheckSpWp]: Trace formula consists of 114 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:27,120 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,199 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 31 trivial. 0 not checked.
[2025-04-28 21:21:27,199 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:28,999 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 24 refuted. 0 times theorem prover too weak. 31 trivial. 0 not checked.
[2025-04-28 21:21:29,000 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1082500394] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:29,000 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:29,000 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 7, 7] total 13
[2025-04-28 21:21:29,000 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [856677938]
[2025-04-28 21:21:29,000 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,001 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:29,001 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,001 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:29,002 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=34, Invalid=122, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:29,002 INFO  L87              Difference]: Start difference. First operand 28 states and 30 transitions. Second operand  has 13 states, 5 states have (on average 3.0) internal successors, (15), 12 states have internal predecessors, (15), 9 states have call successors, (10), 1 states have call predecessors, (10), 4 states have return successors, (10), 4 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:21:29,076 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,077 INFO  L93              Difference]: Finished difference Result 32 states and 34 transitions.
[2025-04-28 21:21:29,077 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:29,078 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 5 states have (on average 3.0) internal successors, (15), 12 states have internal predecessors, (15), 9 states have call successors, (10), 1 states have call predecessors, (10), 4 states have return successors, (10), 4 states have call predecessors, (10), 9 states have call successors, (10) Word has length 32
[2025-04-28 21:21:29,078 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,078 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:29,080 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:29,080 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 79 GetRequests, 60 SyntacticMatches, 6 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 59 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=51, Invalid=159, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:29,081 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 11 mSDsluCounter, 58 mSDsCounter, 0 mSdLazyCounter, 46 mSolverCounterSat, 14 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 72 SdHoareTripleChecker+Invalid, 60 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 14 IncrementalHoareTripleChecker+Valid, 46 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,081 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 72 Invalid, 60 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [14 Valid, 46 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:29,082 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:29,085 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:21:29,085 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 15 states have (on average 1.1333333333333333) internal successors, (17), 16 states have internal predecessors, (17), 7 states have call successors, (7), 6 states have call predecessors, (7), 9 states have return successors, (10), 9 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:29,086 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 34 transitions.
[2025-04-28 21:21:29,086 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 34 transitions. Word has length 32
[2025-04-28 21:21:29,087 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,087 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 34 transitions.
[2025-04-28 21:21:29,087 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 5 states have (on average 3.0) internal successors, (15), 12 states have internal predecessors, (15), 9 states have call successors, (10), 1 states have call predecessors, (10), 4 states have return successors, (10), 4 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:21:29,088 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 34 transitions.
[2025-04-28 21:21:29,089 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:29,089 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,089 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:29,093 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:29,290 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:29,290 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,290 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,290 INFO  L85        PathProgramCache]: Analyzing trace with hash 1983750755, now seen corresponding path program 5 times
[2025-04-28 21:21:29,291 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,291 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [282792009]
[2025-04-28 21:21:29,291 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:29,291 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,307 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:29,363 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:29,366 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:29,366 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,733 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 50 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:21:29,734 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,734 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [282792009]
[2025-04-28 21:21:29,734 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [282792009] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,735 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [587444801]
[2025-04-28 21:21:29,735 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:29,735 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,737 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,740 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:29,745 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,834 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:29,863 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:29,864 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:29,864 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,865 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 27 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,867 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,192 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 5 proven. 48 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:30,192 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,012 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:38,012 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [587444801] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,012 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,013 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 13, 16] total 28
[2025-04-28 21:21:38,013 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1901226066]
[2025-04-28 21:21:38,013 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,014 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 28 states
[2025-04-28 21:21:38,014 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,016 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 28 interpolants.
[2025-04-28 21:21:38,017 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=151, Invalid=605, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:38,017 INFO  L87              Difference]: Start difference. First operand 32 states and 34 transitions. Second operand  has 28 states, 15 states have (on average 2.066666666666667) internal successors, (31), 27 states have internal predecessors, (31), 14 states have call successors, (15), 1 states have call predecessors, (15), 14 states have return successors, (23), 12 states have call predecessors, (23), 14 states have call successors, (23)
[2025-04-28 21:21:38,452 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,452 INFO  L93              Difference]: Finished difference Result 56 states and 59 transitions.
[2025-04-28 21:21:38,453 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:38,453 INFO  L79                 Accepts]: Start accepts. Automaton has  has 28 states, 15 states have (on average 2.066666666666667) internal successors, (31), 27 states have internal predecessors, (31), 14 states have call successors, (15), 1 states have call predecessors, (15), 14 states have return successors, (23), 12 states have call predecessors, (23), 14 states have call successors, (23) Word has length 36
[2025-04-28 21:21:38,455 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,456 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:38,456 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:38,457 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 97 GetRequests, 60 SyntacticMatches, 1 SemanticMatches, 36 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 394 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=365, Invalid=1041, Unknown=0, NotChecked=0, Total=1406
[2025-04-28 21:21:38,457 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 75 mSDsluCounter, 123 mSDsCounter, 0 mSdLazyCounter, 67 mSolverCounterSat, 82 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 76 SdHoareTripleChecker+Valid, 138 SdHoareTripleChecker+Invalid, 149 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 82 IncrementalHoareTripleChecker+Valid, 67 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,459 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [76 Valid, 138 Invalid, 149 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [82 Valid, 67 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:38,460 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:38,468 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 40.
[2025-04-28 21:21:38,468 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 19 states have (on average 1.105263157894737) internal successors, (21), 20 states have internal predecessors, (21), 7 states have call successors, (7), 6 states have call predecessors, (7), 13 states have return successors, (14), 13 states have call predecessors, (14), 7 states have call successors, (14)
[2025-04-28 21:21:38,469 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 42 transitions.
[2025-04-28 21:21:38,469 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 42 transitions. Word has length 36
[2025-04-28 21:21:38,469 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,469 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 42 transitions.
[2025-04-28 21:21:38,469 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 28 states, 15 states have (on average 2.066666666666667) internal successors, (31), 27 states have internal predecessors, (31), 14 states have call successors, (15), 1 states have call predecessors, (15), 14 states have return successors, (23), 12 states have call predecessors, (23), 14 states have call successors, (23)
[2025-04-28 21:21:38,473 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 42 transitions.
[2025-04-28 21:21:38,474 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:38,474 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,474 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,481 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:38,675 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:38,675 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,675 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,675 INFO  L85        PathProgramCache]: Analyzing trace with hash 1660611179, now seen corresponding path program 6 times
[2025-04-28 21:21:38,675 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,675 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [202842677]
[2025-04-28 21:21:38,676 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:38,676 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,682 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 52 statements into 11 equivalence classes.
[2025-04-28 21:21:38,717 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:38,718 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s)
[2025-04-28 21:21:38,718 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,479 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 19 proven. 124 refuted. 0 times theorem prover too weak. 67 trivial. 0 not checked.
[2025-04-28 21:21:39,479 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,479 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [202842677]
[2025-04-28 21:21:39,479 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [202842677] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,480 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1516425506]
[2025-04-28 21:21:39,480 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:39,480 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,483 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,484 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:39,487 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,623 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 52 statements into 11 equivalence classes.
[2025-04-28 21:21:39,668 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:39,668 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s)
[2025-04-28 21:21:39,668 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,670 INFO  L256         TraceCheckSpWp]: Trace formula consists of 194 conjuncts, 44 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,674 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,168 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 15 proven. 127 refuted. 0 times theorem prover too weak. 68 trivial. 0 not checked.
[2025-04-28 21:21:40,168 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
