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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:23,535 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:23,632 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_34f5442d-c995-457f-86be-7d37d955c493/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:23,638 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:23,638 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:23,672 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:23,673 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:23,674 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:23,674 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:23,675 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:23,676 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:23,676 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:23,676 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:23,676 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:23,676 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:23,676 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:23,676 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:23,677 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:23,677 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:23,677 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:23,677 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:23,677 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:23,677 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:23,677 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:23,677 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:23,678 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:23,678 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:24,035 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:24,048 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:24,050 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:24,053 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:24,054 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:24,055 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_34f5442d-c995-457f-86be-7d37d955c493/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-209.smt2
[2025-04-28 21:21:24,058 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:24,061 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:24,338 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_34f5442d-c995-457f-86be-7d37d955c493/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-209.smt2
[2025-04-28 21:21:24,341 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:24,342 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:24,343 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:24,343 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:24,343 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:24,346 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,380 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24 Unit
[2025-04-28 21:21:24,380 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:24,381 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:24,381 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:24,381 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:24,399 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,399 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,427 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,427 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,430 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,431 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,433 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,435 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,436 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,456 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:24,459 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:24,459 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:24,459 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:24,460 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (1/1) ...
[2025-04-28 21:21:24,462 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:24,475 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:24,489 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:24,492 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:24,507 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:24,508 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:24,508 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:24,508 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV1 given in one single declaration
[2025-04-28 21:21:24,508 INFO  L130     BoogieDeclarations]: Found specification of procedure INV1
[2025-04-28 21:21:24,508 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV1
[2025-04-28 21:21:24,508 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:24,508 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:24,508 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:24,567 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:24,572 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:24,770 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:24,771 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:24,787 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:24,788 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:24,788 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:24 BoogieIcfgContainer
[2025-04-28 21:21:24,788 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:24,791 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:24,795 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:24,802 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:24,803 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:24" (1/3) ...
[2025-04-28 21:21:24,803 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6c616406 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:24, skipping insertion in model container
[2025-04-28 21:21:24,804 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:24" (2/3) ...
[2025-04-28 21:21:24,804 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6c616406 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:24, skipping insertion in model container
[2025-04-28 21:21:24,804 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:24" (3/3) ...
[2025-04-28 21:21:24,805 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:24,822 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:24,825 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 17 locations, 33 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:24,879 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:24,893 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;@66296a5c, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:24,895 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:24,899 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 17 states, 6 states have (on average 2.0) internal successors, (12), 12 states have internal predecessors, (12), 7 states have call successors, (7), 2 states have call predecessors, (7), 2 states have return successors, (7), 3 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:24,909 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:24,911 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,914 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:24,914 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,919 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,919 INFO  L85        PathProgramCache]: Analyzing trace with hash -572989311, now seen corresponding path program 1 times
[2025-04-28 21:21:24,927 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,928 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [96208294]
[2025-04-28 21:21:24,928 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,929 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,969 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:24,998 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:24,999 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,999 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,158 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:25,159 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,159 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [96208294]
[2025-04-28 21:21:25,160 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [96208294] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:25,160 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:25,163 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:25,167 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [749757346]
[2025-04-28 21:21:25,167 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,172 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:25,174 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,202 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:25,203 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:25,205 INFO  L87              Difference]: Start difference. First operand  has 17 states, 6 states have (on average 2.0) internal successors, (12), 12 states have internal predecessors, (12), 7 states have call successors, (7), 2 states have call predecessors, (7), 2 states have return successors, (7), 3 states have call predecessors, (7), 7 states have call successors, (7) Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:25,315 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,316 INFO  L93              Difference]: Finished difference Result 17 states and 30 transitions.
[2025-04-28 21:21:25,317 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:25,319 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:25,319 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,324 INFO  L225             Difference]: With dead ends: 17
[2025-04-28 21:21:25,325 INFO  L226             Difference]: Without dead ends: 17
[2025-04-28 21:21:25,347 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:25,350 INFO  L437           NwaCegarLoop]: 19 mSDtfsCounter, 1 mSDsluCounter, 23 mSDsCounter, 0 mSdLazyCounter, 26 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 42 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 26 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:25,351 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 42 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 26 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:25,365 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17 states.
[2025-04-28 21:21:25,411 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 17 to 17.
[2025-04-28 21:21:25,412 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 17 states, 6 states have (on average 1.8333333333333333) internal successors, (11), 11 states have internal predecessors, (11), 7 states have call successors, (7), 2 states have call predecessors, (7), 3 states have return successors, (12), 3 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:25,418 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 30 transitions.
[2025-04-28 21:21:25,421 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 30 transitions. Word has length 9
[2025-04-28 21:21:25,422 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,422 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 30 transitions.
[2025-04-28 21:21:25,422 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:25,422 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 30 transitions.
[2025-04-28 21:21:25,426 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:25,426 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,427 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:25,427 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:25,427 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,428 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,428 INFO  L85        PathProgramCache]: Analyzing trace with hash -573690710, now seen corresponding path program 1 times
[2025-04-28 21:21:25,428 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,428 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [109626009]
[2025-04-28 21:21:25,428 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,431 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,447 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:25,486 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:25,486 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,486 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,348 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:26,348 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,349 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [109626009]
[2025-04-28 21:21:26,349 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [109626009] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:26,349 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1860449127]
[2025-04-28 21:21:26,349 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,350 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:26,353 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:26,358 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:26,361 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:26,411 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:26,447 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:26,447 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,447 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,451 INFO  L256         TraceCheckSpWp]: Trace formula consists of 122 conjuncts, 29 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:26,459 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:26,624 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:26,625 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:27,279 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:27,279 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1860449127] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:27,281 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:27,281 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 11
[2025-04-28 21:21:27,282 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1015047834]
[2025-04-28 21:21:27,282 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,283 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:27,283 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,284 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:27,284 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=27, Invalid=83, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:27,286 INFO  L87              Difference]: Start difference. First operand 17 states and 30 transitions. Second operand  has 11 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 10 states have internal predecessors, (13), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 3 states have call predecessors, (6), 6 states have call successors, (6)
[2025-04-28 21:21:27,710 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,710 INFO  L93              Difference]: Finished difference Result 21 states and 43 transitions.
[2025-04-28 21:21:27,715 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:27,715 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 10 states have internal predecessors, (13), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 3 states have call predecessors, (6), 6 states have call successors, (6) Word has length 13
[2025-04-28 21:21:27,716 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,717 INFO  L225             Difference]: With dead ends: 21
[2025-04-28 21:21:27,717 INFO  L226             Difference]: Without dead ends: 21
[2025-04-28 21:21:27,718 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 34 GetRequests, 22 SyntacticMatches, 0 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=47, Invalid=135, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:27,719 INFO  L437           NwaCegarLoop]: 20 mSDtfsCounter, 5 mSDsluCounter, 67 mSDsCounter, 0 mSdLazyCounter, 129 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 87 SdHoareTripleChecker+Invalid, 145 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 129 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,720 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 87 Invalid, 145 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 129 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:27,721 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 21 states.
[2025-04-28 21:21:27,727 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 21 to 19.
[2025-04-28 21:21:27,727 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 19 states, 7 states have (on average 1.7142857142857142) internal successors, (12), 12 states have internal predecessors, (12), 7 states have call successors, (7), 2 states have call predecessors, (7), 4 states have return successors, (17), 4 states have call predecessors, (17), 7 states have call successors, (17)
[2025-04-28 21:21:27,728 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 19 states to 19 states and 36 transitions.
[2025-04-28 21:21:27,728 INFO  L79                 Accepts]: Start accepts. Automaton has 19 states and 36 transitions. Word has length 13
[2025-04-28 21:21:27,728 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,729 INFO  L485      AbstractCegarLoop]: Abstraction has 19 states and 36 transitions.
[2025-04-28 21:21:27,729 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 10 states have internal predecessors, (13), 6 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 3 states have call predecessors, (6), 6 states have call successors, (6)
[2025-04-28 21:21:27,729 INFO  L278                IsEmpty]: Start isEmpty. Operand 19 states and 36 transitions.
[2025-04-28 21:21:27,730 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:27,730 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,730 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,735 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:27,931 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:27,931 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,931 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,932 INFO  L85        PathProgramCache]: Analyzing trace with hash 162061849, now seen corresponding path program 1 times
[2025-04-28 21:21:27,932 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,932 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [310450897]
[2025-04-28 21:21:27,932 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,932 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,938 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:27,942 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:27,942 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,943 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,045 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:28,045 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,045 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [310450897]
[2025-04-28 21:21:28,045 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [310450897] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,045 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [904314979]
[2025-04-28 21:21:28,045 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,045 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,050 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,052 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:28,056 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,096 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:28,128 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:28,128 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,128 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,133 INFO  L256         TraceCheckSpWp]: Trace formula consists of 115 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,135 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,279 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:28,279 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:29,429 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:29,430 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [904314979] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,430 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:29,430 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6, 6] total 12
[2025-04-28 21:21:29,430 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1191071138]
[2025-04-28 21:21:29,430 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,431 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:29,431 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,431 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:29,431 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=27, Invalid=105, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:29,432 INFO  L87              Difference]: Start difference. First operand 19 states and 36 transitions. Second operand  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:29,566 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,566 INFO  L93              Difference]: Finished difference Result 25 states and 55 transitions.
[2025-04-28 21:21:29,567 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:29,567 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-04-28 21:21:29,568 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,570 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:21:29,570 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:21:29,571 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 31 GetRequests, 21 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=27, Invalid=105, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:29,571 INFO  L437           NwaCegarLoop]: 19 mSDtfsCounter, 2 mSDsluCounter, 27 mSDsCounter, 0 mSdLazyCounter, 60 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 46 SdHoareTripleChecker+Invalid, 64 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 60 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,572 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 46 Invalid, 64 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 60 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:29,574 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:21:29,584 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 21.
[2025-04-28 21:21:29,584 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 21 states, 8 states have (on average 1.625) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 2 states have call predecessors, (7), 5 states have return successors, (22), 5 states have call predecessors, (22), 7 states have call successors, (22)
[2025-04-28 21:21:29,588 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 21 states to 21 states and 42 transitions.
[2025-04-28 21:21:29,588 INFO  L79                 Accepts]: Start accepts. Automaton has 21 states and 42 transitions. Word has length 13
[2025-04-28 21:21:29,589 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,589 INFO  L485      AbstractCegarLoop]: Abstraction has 21 states and 42 transitions.
[2025-04-28 21:21:29,589 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:29,589 INFO  L278                IsEmpty]: Start isEmpty. Operand 21 states and 42 transitions.
[2025-04-28 21:21:29,590 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:29,590 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,590 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:29,596 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:29,790 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,791 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,791 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,791 INFO  L85        PathProgramCache]: Analyzing trace with hash -83189004, now seen corresponding path program 1 times
[2025-04-28 21:21:29,791 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,791 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [485435828]
[2025-04-28 21:21:29,791 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,792 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,796 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:29,801 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:29,801 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,801 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,887 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:29,887 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,888 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [485435828]
[2025-04-28 21:21:29,888 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [485435828] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,888 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1916457422]
[2025-04-28 21:21:29,888 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,888 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,890 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,893 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:29,897 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,936 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:29,959 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:29,959 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,959 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,960 INFO  L256         TraceCheckSpWp]: Trace formula consists of 116 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,962 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,078 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:30,079 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:31,000 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:31,000 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1916457422] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,000 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:31,001 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6, 6] total 12
[2025-04-28 21:21:31,001 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1769963774]
[2025-04-28 21:21:31,001 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,001 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:31,001 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,002 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:31,002 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=27, Invalid=105, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:31,002 INFO  L87              Difference]: Start difference. First operand 21 states and 42 transitions. Second operand  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:31,120 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,120 INFO  L93              Difference]: Finished difference Result 27 states and 61 transitions.
[2025-04-28 21:21:31,121 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:31,121 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-04-28 21:21:31,121 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,122 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:31,122 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:31,123 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 31 GetRequests, 21 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=27, Invalid=105, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:31,123 INFO  L437           NwaCegarLoop]: 19 mSDtfsCounter, 2 mSDsluCounter, 26 mSDsCounter, 0 mSdLazyCounter, 58 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 45 SdHoareTripleChecker+Invalid, 64 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 58 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,126 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 45 Invalid, 64 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 58 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:31,126 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:31,137 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 23.
[2025-04-28 21:21:31,141 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 23 states, 9 states have (on average 1.5555555555555556) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 2 states have call predecessors, (7), 6 states have return successors, (27), 6 states have call predecessors, (27), 7 states have call successors, (27)
[2025-04-28 21:21:31,142 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 23 states to 23 states and 48 transitions.
[2025-04-28 21:21:31,144 INFO  L79                 Accepts]: Start accepts. Automaton has 23 states and 48 transitions. Word has length 13
[2025-04-28 21:21:31,144 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,144 INFO  L485      AbstractCegarLoop]: Abstraction has 23 states and 48 transitions.
[2025-04-28 21:21:31,145 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:31,145 INFO  L278                IsEmpty]: Start isEmpty. Operand 23 states and 48 transitions.
[2025-04-28 21:21:31,146 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:31,146 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,146 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,153 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:31,351 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,351 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,351 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,351 INFO  L85        PathProgramCache]: Analyzing trace with hash -912992212, now seen corresponding path program 1 times
[2025-04-28 21:21:31,351 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,351 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2048117966]
[2025-04-28 21:21:31,352 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,352 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,357 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:31,363 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:31,363 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,363 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,418 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:31,418 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,419 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2048117966]
[2025-04-28 21:21:31,419 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2048117966] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,419 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1964440678]
[2025-04-28 21:21:31,419 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,419 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,421 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,424 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:31,429 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,472 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:31,497 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:31,498 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,498 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,499 INFO  L256         TraceCheckSpWp]: Trace formula consists of 174 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,500 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,515 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:31,515 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:31,716 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:31,717 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1964440678] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:31,717 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:31,717 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:31,717 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2147247784]
[2025-04-28 21:21:31,717 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,718 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:31,718 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,718 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:31,718 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=36, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:31,719 INFO  L87              Difference]: Start difference. First operand 23 states and 48 transitions. Second operand  has 8 states, 4 states have (on average 2.75) internal successors, (11), 8 states have internal predecessors, (11), 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:31,902 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,902 INFO  L93              Difference]: Finished difference Result 31 states and 71 transitions.
[2025-04-28 21:21:31,903 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:31,903 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.75) internal successors, (11), 8 states have internal predecessors, (11), 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 17
[2025-04-28 21:21:31,904 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,906 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:31,906 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:31,907 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 41 GetRequests, 31 SyntacticMatches, 2 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=31, Invalid=59, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:31,907 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 4 mSDsluCounter, 66 mSDsCounter, 0 mSdLazyCounter, 139 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 88 SdHoareTripleChecker+Invalid, 145 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 139 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,908 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 88 Invalid, 145 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 139 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:31,908 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:31,918 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 25.
[2025-04-28 21:21:31,919 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 25 states, 10 states have (on average 1.5) internal successors, (15), 15 states have internal predecessors, (15), 7 states have call successors, (7), 2 states have call predecessors, (7), 7 states have return successors, (29), 7 states have call predecessors, (29), 7 states have call successors, (29)
[2025-04-28 21:21:31,920 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 51 transitions.
[2025-04-28 21:21:31,920 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 51 transitions. Word has length 17
[2025-04-28 21:21:31,920 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,920 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 51 transitions.
[2025-04-28 21:21:31,920 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.75) internal successors, (11), 8 states have internal predecessors, (11), 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:31,920 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 51 transitions.
[2025-04-28 21:21:31,922 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:31,922 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,922 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,930 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:32,122 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:32,123 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,123 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,123 INFO  L85        PathProgramCache]: Analyzing trace with hash 680212957, now seen corresponding path program 1 times
[2025-04-28 21:21:32,123 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,123 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1163426088]
[2025-04-28 21:21:32,123 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,123 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,130 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:32,137 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:32,137 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,138 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,269 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:32,269 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,269 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1163426088]
[2025-04-28 21:21:32,270 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1163426088] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:32,270 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1298982620]
[2025-04-28 21:21:32,270 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,270 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,272 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:32,274 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:32,281 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:32,324 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:32,350 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:32,351 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,351 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,352 INFO  L256         TraceCheckSpWp]: Trace formula consists of 167 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:32,354 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,521 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:32,522 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:34,546 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:34,546 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1298982620] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:34,546 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:34,546 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 16
[2025-04-28 21:21:34,547 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1879892035]
[2025-04-28 21:21:34,547 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,547 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:34,547 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,548 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:34,549 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=200, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:34,549 INFO  L87              Difference]: Start difference. First operand 25 states and 51 transitions. Second operand  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (10), 6 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:21:35,230 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,231 INFO  L93              Difference]: Finished difference Result 43 states and 111 transitions.
[2025-04-28 21:21:35,231 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:35,231 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (10), 6 states have call predecessors, (10), 9 states have call successors, (10) Word has length 17
[2025-04-28 21:21:35,232 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,233 INFO  L225             Difference]: With dead ends: 43
[2025-04-28 21:21:35,233 INFO  L226             Difference]: Without dead ends: 43
[2025-04-28 21:21:35,233 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 27 SyntacticMatches, 0 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 57 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=93, Invalid=459, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:35,234 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 13 mSDsluCounter, 119 mSDsCounter, 0 mSdLazyCounter, 403 mSolverCounterSat, 50 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 41 SdHoareTripleChecker+Valid, 142 SdHoareTripleChecker+Invalid, 453 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 50 IncrementalHoareTripleChecker+Valid, 403 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,237 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [41 Valid, 142 Invalid, 453 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [50 Valid, 403 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:35,239 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 43 states.
[2025-04-28 21:21:35,263 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 43 to 27.
[2025-04-28 21:21:35,264 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.4545454545454546) internal successors, (16), 16 states have internal predecessors, (16), 7 states have call successors, (7), 2 states have call predecessors, (7), 8 states have return successors, (35), 8 states have call predecessors, (35), 7 states have call successors, (35)
[2025-04-28 21:21:35,265 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 58 transitions.
[2025-04-28 21:21:35,265 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 58 transitions. Word has length 17
[2025-04-28 21:21:35,265 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,265 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 58 transitions.
[2025-04-28 21:21:35,265 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (10), 6 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:21:35,265 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 58 transitions.
[2025-04-28 21:21:35,266 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:35,266 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,267 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,273 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:35,467 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:35,467 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,467 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,468 INFO  L85        PathProgramCache]: Analyzing trace with hash -557413502, now seen corresponding path program 1 times
[2025-04-28 21:21:35,468 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,468 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [817517328]
[2025-04-28 21:21:35,468 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,468 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,472 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:35,477 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:35,478 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,478 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,624 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:35,624 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,625 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [817517328]
[2025-04-28 21:21:35,625 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [817517328] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:35,625 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [720165411]
[2025-04-28 21:21:35,625 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,625 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:35,628 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,630 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:35,633 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:35,690 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:35,711 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:35,711 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,711 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,713 INFO  L256         TraceCheckSpWp]: Trace formula consists of 166 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:35,714 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:35,846 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:35,846 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:37,731 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:37,731 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [720165411] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:37,731 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:37,731 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 16
[2025-04-28 21:21:37,731 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [973775382]
[2025-04-28 21:21:37,732 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,732 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:37,732 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,733 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:37,733 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=200, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:37,733 INFO  L87              Difference]: Start difference. First operand 27 states and 58 transitions. Second operand  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (10), 6 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:21:38,338 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,338 INFO  L93              Difference]: Finished difference Result 49 states and 130 transitions.
[2025-04-28 21:21:38,339 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:38,339 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (10), 6 states have call predecessors, (10), 9 states have call successors, (10) Word has length 17
[2025-04-28 21:21:38,339 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,341 INFO  L225             Difference]: With dead ends: 49
[2025-04-28 21:21:38,341 INFO  L226             Difference]: Without dead ends: 49
[2025-04-28 21:21:38,342 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 27 SyntacticMatches, 0 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 56 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=93, Invalid=459, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:38,342 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 12 mSDsluCounter, 107 mSDsCounter, 0 mSdLazyCounter, 363 mSolverCounterSat, 55 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 33 SdHoareTripleChecker+Valid, 130 SdHoareTripleChecker+Invalid, 418 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 55 IncrementalHoareTripleChecker+Valid, 363 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,342 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [33 Valid, 130 Invalid, 418 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [55 Valid, 363 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:38,343 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 49 states.
[2025-04-28 21:21:38,356 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 49 to 33.
[2025-04-28 21:21:38,356 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 14 states have (on average 1.3571428571428572) internal successors, (19), 19 states have internal predecessors, (19), 7 states have call successors, (7), 2 states have call predecessors, (7), 11 states have return successors, (50), 11 states have call predecessors, (50), 7 states have call successors, (50)
[2025-04-28 21:21:38,357 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 76 transitions.
[2025-04-28 21:21:38,357 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 76 transitions. Word has length 17
[2025-04-28 21:21:38,358 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,358 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 76 transitions.
[2025-04-28 21:21:38,358 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (10), 6 states have call predecessors, (10), 9 states have call successors, (10)
[2025-04-28 21:21:38,358 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 76 transitions.
[2025-04-28 21:21:38,359 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:38,359 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,359 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,367 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:38,560 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,560 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,560 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,560 INFO  L85        PathProgramCache]: Analyzing trace with hash -1139501421, now seen corresponding path program 2 times
[2025-04-28 21:21:38,560 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,561 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1185877354]
[2025-04-28 21:21:38,561 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:38,561 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,567 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:38,581 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:38,582 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:38,582 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,099 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:39,099 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,099 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1185877354]
[2025-04-28 21:21:39,099 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1185877354] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,099 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [715396131]
[2025-04-28 21:21:39,099 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:39,100 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,102 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,104 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:39,110 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,174 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:39,201 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:39,202 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:39,202 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,204 INFO  L256         TraceCheckSpWp]: Trace formula consists of 173 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,205 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,423 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 1 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:39,423 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,509 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:40,510 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [715396131] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,510 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,510 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 17
[2025-04-28 21:21:40,510 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1865140699]
[2025-04-28 21:21:40,510 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,510 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:40,511 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,511 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:40,511 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=43, Invalid=229, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:40,511 INFO  L87              Difference]: Start difference. First operand 33 states and 76 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, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 5 states have call predecessors, (10), 10 states have call successors, (10)
[2025-04-28 21:21:41,347 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,348 INFO  L93              Difference]: Finished difference Result 61 states and 163 transitions.
[2025-04-28 21:21:41,348 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:41,348 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, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 5 states have call predecessors, (10), 10 states have call successors, (10) Word has length 17
[2025-04-28 21:21:41,349 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,351 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:41,351 INFO  L226             Difference]: Without dead ends: 61
[2025-04-28 21:21:41,351 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 25 SyntacticMatches, 1 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 66 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=123, Invalid=477, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:41,352 INFO  L437           NwaCegarLoop]: 20 mSDtfsCounter, 21 mSDsluCounter, 86 mSDsCounter, 0 mSdLazyCounter, 237 mSolverCounterSat, 46 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 106 SdHoareTripleChecker+Invalid, 283 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 46 IncrementalHoareTripleChecker+Valid, 237 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,352 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 106 Invalid, 283 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [46 Valid, 237 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:41,353 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 61 states.
[2025-04-28 21:21:41,366 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 61 to 37.
[2025-04-28 21:21:41,366 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 37 states, 16 states have (on average 1.3125) internal successors, (21), 21 states have internal predecessors, (21), 7 states have call successors, (7), 2 states have call predecessors, (7), 13 states have return successors, (60), 13 states have call predecessors, (60), 7 states have call successors, (60)
[2025-04-28 21:21:41,367 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 37 states to 37 states and 88 transitions.
[2025-04-28 21:21:41,368 INFO  L79                 Accepts]: Start accepts. Automaton has 37 states and 88 transitions. Word has length 17
[2025-04-28 21:21:41,368 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,368 INFO  L485      AbstractCegarLoop]: Abstraction has 37 states and 88 transitions.
[2025-04-28 21:21:41,368 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, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 5 states have call predecessors, (10), 10 states have call successors, (10)
[2025-04-28 21:21:41,368 INFO  L278                IsEmpty]: Start isEmpty. Operand 37 states and 88 transitions.
[2025-04-28 21:21:41,369 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:41,369 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,370 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,376 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:41,570 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable8
[2025-04-28 21:21:41,570 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,571 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,571 INFO  L85        PathProgramCache]: Analyzing trace with hash 1544071234, now seen corresponding path program 2 times
[2025-04-28 21:21:41,571 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,571 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [704730251]
[2025-04-28 21:21:41,571 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:41,571 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,574 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:41,578 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:41,578 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:41,579 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,608 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:41,609 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,609 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [704730251]
[2025-04-28 21:21:41,609 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [704730251] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,609 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,609 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:41,609 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [320824583]
[2025-04-28 21:21:41,609 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,610 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:41,610 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,610 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:41,610 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:41,610 INFO  L87              Difference]: Start difference. First operand 37 states and 88 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:41,740 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,740 INFO  L93              Difference]: Finished difference Result 56 states and 132 transitions.
[2025-04-28 21:21:41,741 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:41,741 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:21:41,741 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,743 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:41,743 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:41,743 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:41,743 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 7 mSDsluCounter, 17 mSDsCounter, 0 mSdLazyCounter, 69 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 46 SdHoareTripleChecker+Invalid, 77 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 69 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,744 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 46 Invalid, 77 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 69 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:41,744 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:41,752 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 36.
[2025-04-28 21:21:41,752 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 14 states have (on average 1.7142857142857142) internal successors, (24), 23 states have internal predecessors, (24), 11 states have call successors, (11), 3 states have call predecessors, (11), 10 states have return successors, (61), 10 states have call predecessors, (61), 11 states have call successors, (61)
[2025-04-28 21:21:41,753 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 96 transitions.
[2025-04-28 21:21:41,753 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 96 transitions. Word has length 17
[2025-04-28 21:21:41,753 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,753 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 96 transitions.
[2025-04-28 21:21:41,754 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:41,754 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 96 transitions.
[2025-04-28 21:21:41,755 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:41,755 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,755 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,755 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:41,760 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,760 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,760 INFO  L85        PathProgramCache]: Analyzing trace with hash -1987255306, now seen corresponding path program 1 times
[2025-04-28 21:21:41,760 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,760 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1336913238]
[2025-04-28 21:21:41,760 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,760 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,764 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:41,770 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:41,774 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,774 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,808 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:41,809 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,809 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1336913238]
[2025-04-28 21:21:41,809 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1336913238] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,809 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,809 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:41,810 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [547244647]
[2025-04-28 21:21:41,810 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,810 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:41,810 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,811 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:41,811 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:41,811 INFO  L87              Difference]: Start difference. First operand 36 states and 96 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:41,941 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,941 INFO  L93              Difference]: Finished difference Result 54 states and 113 transitions.
[2025-04-28 21:21:41,942 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:41,942 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:21:41,943 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,943 INFO  L225             Difference]: With dead ends: 54
[2025-04-28 21:21:41,943 INFO  L226             Difference]: Without dead ends: 20
[2025-04-28 21:21:41,943 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:41,944 INFO  L437           NwaCegarLoop]: 25 mSDtfsCounter, 6 mSDsluCounter, 16 mSDsCounter, 0 mSdLazyCounter, 60 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 41 SdHoareTripleChecker+Invalid, 70 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 60 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,944 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 41 Invalid, 70 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 60 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:41,945 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 20 states.
[2025-04-28 21:21:41,949 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 20 to 20.
[2025-04-28 21:21:41,952 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 20 states, 9 states have (on average 1.2222222222222223) internal successors, (11), 11 states have internal predecessors, (11), 4 states have call successors, (4), 2 states have call predecessors, (4), 6 states have return successors, (10), 6 states have call predecessors, (10), 4 states have call successors, (10)
[2025-04-28 21:21:41,952 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 25 transitions.
[2025-04-28 21:21:41,952 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 25 transitions. Word has length 17
[2025-04-28 21:21:41,952 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,953 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 25 transitions.
[2025-04-28 21:21:41,953 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:41,953 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 25 transitions.
[2025-04-28 21:21:41,953 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:41,953 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,953 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,954 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:41,954 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,954 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,954 INFO  L85        PathProgramCache]: Analyzing trace with hash 581370789, now seen corresponding path program 3 times
[2025-04-28 21:21:41,954 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,954 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [571699451]
[2025-04-28 21:21:41,954 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:41,954 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,964 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 25 statements into 5 equivalence classes.
[2025-04-28 21:21:41,988 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 5 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:41,990 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 5 check-sat command(s)
[2025-04-28 21:21:41,990 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,489 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:42,489 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,489 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [571699451]
[2025-04-28 21:21:42,489 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [571699451] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,489 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1353304193]
[2025-04-28 21:21:42,489 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:42,490 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,492 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,494 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:42,498 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,565 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 25 statements into 5 equivalence classes.
[2025-04-28 21:21:42,609 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 5 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:42,609 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 5 check-sat command(s)
[2025-04-28 21:21:42,609 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,614 INFO  L256         TraceCheckSpWp]: Trace formula consists of 275 conjuncts, 123 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,616 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,317 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 2 proven. 24 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:43,317 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,406 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:48,406 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1353304193] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,406 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,406 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 28
[2025-04-28 21:21:48,407 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [804553754]
[2025-04-28 21:21:48,407 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,407 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 28 states
[2025-04-28 21:21:48,407 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,408 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 28 interpolants.
[2025-04-28 21:21:48,408 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=89, Invalid=667, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:48,408 INFO  L87              Difference]: Start difference. First operand 20 states and 25 transitions. Second operand  has 28 states, 13 states have (on average 2.3076923076923075) internal successors, (30), 27 states have internal predecessors, (30), 16 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (16), 10 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:49,773 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,774 INFO  L93              Difference]: Finished difference Result 30 states and 41 transitions.
[2025-04-28 21:21:49,774 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:49,775 INFO  L79                 Accepts]: Start accepts. Automaton has  has 28 states, 13 states have (on average 2.3076923076923075) internal successors, (30), 27 states have internal predecessors, (30), 16 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (16), 10 states have call predecessors, (16), 16 states have call successors, (16) Word has length 25
[2025-04-28 21:21:49,775 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,775 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:49,775 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:49,776 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 70 GetRequests, 34 SyntacticMatches, 1 SemanticMatches, 35 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 162 ImplicationChecksByTransitivity, 1.8s TimeCoverageRelationStatistics Valid=251, Invalid=1081, Unknown=0, NotChecked=0, Total=1332
[2025-04-28 21:21:49,776 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 63 mSDsluCounter, 150 mSDsCounter, 0 mSdLazyCounter, 200 mSolverCounterSat, 153 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 65 SdHoareTripleChecker+Valid, 166 SdHoareTripleChecker+Invalid, 353 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 153 IncrementalHoareTripleChecker+Valid, 200 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,776 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [65 Valid, 166 Invalid, 353 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [153 Valid, 200 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:49,777 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:49,780 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 22.
[2025-04-28 21:21:49,780 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 10 states have (on average 1.2) internal successors, (12), 12 states have internal predecessors, (12), 4 states have call successors, (4), 2 states have call predecessors, (4), 7 states have return successors, (12), 7 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:49,780 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 28 transitions.
[2025-04-28 21:21:49,780 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 28 transitions. Word has length 25
[2025-04-28 21:21:49,781 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,781 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 28 transitions.
[2025-04-28 21:21:49,781 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 28 states, 13 states have (on average 2.3076923076923075) internal successors, (30), 27 states have internal predecessors, (30), 16 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (16), 10 states have call predecessors, (16), 16 states have call successors, (16)
[2025-04-28 21:21:49,781 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 28 transitions.
[2025-04-28 21:21:49,781 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:49,781 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,782 INFO  L218           NwaCegarLoop]: trace histogram [6, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,788 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:49,982 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-04-28 21:21:49,982 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,983 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,983 INFO  L85        PathProgramCache]: Analyzing trace with hash -44917977, now seen corresponding path program 2 times
[2025-04-28 21:21:49,983 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,983 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [47573427]
[2025-04-28 21:21:49,983 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:49,983 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,991 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:50,010 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:50,010 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:50,010 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,332 INFO  L134       CoverageAnalysis]: Checked inductivity of 51 backedges. 0 proven. 36 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:50,332 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,332 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [47573427]
[2025-04-28 21:21:50,332 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [47573427] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,333 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1004851610]
[2025-04-28 21:21:50,333 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:50,333 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,336 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,338 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:50,341 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,450 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:50,525 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:50,525 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:50,525 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,529 INFO  L256         TraceCheckSpWp]: Trace formula consists of 327 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,531 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,702 INFO  L134       CoverageAnalysis]: Checked inductivity of 51 backedges. 19 proven. 12 refuted. 0 times theorem prover too weak. 20 trivial. 0 not checked.
[2025-04-28 21:21:50,702 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,586 INFO  L134       CoverageAnalysis]: Checked inductivity of 51 backedges. 19 proven. 15 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-04-28 21:21:51,586 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1004851610] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,586 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,586 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 8, 10] total 24
[2025-04-28 21:21:51,586 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1397968063]
[2025-04-28 21:21:51,586 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,587 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:21:51,587 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,588 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:21:51,588 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=74, Invalid=478, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:51,588 INFO  L87              Difference]: Start difference. First operand 22 states and 28 transitions. Second operand  has 24 states, 12 states have (on average 2.4166666666666665) internal successors, (29), 24 states have internal predecessors, (29), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (17), 9 states have call predecessors, (17), 13 states have call successors, (17)
[2025-04-28 21:21:51,861 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,861 INFO  L93              Difference]: Finished difference Result 26 states and 33 transitions.
[2025-04-28 21:21:51,861 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:51,862 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.4166666666666665) internal successors, (29), 24 states have internal predecessors, (29), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (17), 9 states have call predecessors, (17), 13 states have call successors, (17) Word has length 29
[2025-04-28 21:21:51,862 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,862 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:51,862 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:51,863 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 78 GetRequests, 46 SyntacticMatches, 4 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 108 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=157, Invalid=713, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:51,863 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 25 mSDsluCounter, 114 mSDsCounter, 0 mSdLazyCounter, 143 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 27 SdHoareTripleChecker+Valid, 128 SdHoareTripleChecker+Invalid, 184 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 143 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,863 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [27 Valid, 128 Invalid, 184 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 143 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:51,864 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:51,866 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 24.
[2025-04-28 21:21:51,866 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 13 states have internal predecessors, (13), 4 states have call successors, (4), 2 states have call predecessors, (4), 8 states have return successors, (12), 8 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:51,867 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 29 transitions.
[2025-04-28 21:21:51,867 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 29 transitions. Word has length 29
[2025-04-28 21:21:51,867 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,867 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 29 transitions.
[2025-04-28 21:21:51,867 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.4166666666666665) internal successors, (29), 24 states have internal predecessors, (29), 13 states have call successors, (15), 1 states have call predecessors, (15), 11 states have return successors, (17), 9 states have call predecessors, (17), 13 states have call successors, (17)
[2025-04-28 21:21:51,868 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 29 transitions.
[2025-04-28 21:21:51,868 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:51,868 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,868 INFO  L218           NwaCegarLoop]: trace histogram [7, 4, 4, 4, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,874 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:52,073 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:52,073 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,073 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,073 INFO  L85        PathProgramCache]: Analyzing trace with hash 522879529, now seen corresponding path program 3 times
[2025-04-28 21:21:52,073 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,073 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [289901756]
[2025-04-28 21:21:52,073 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:52,074 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,081 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:52,088 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 21 of 33 statements.
[2025-04-28 21:21:52,088 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:52,088 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,136 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 22 proven. 1 refuted. 0 times theorem prover too weak. 47 trivial. 0 not checked.
[2025-04-28 21:21:52,136 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,136 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [289901756]
[2025-04-28 21:21:52,136 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [289901756] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,136 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1120221670]
[2025-04-28 21:21:52,136 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:52,136 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,139 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,141 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,144 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,238 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:52,281 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 21 of 33 statements.
[2025-04-28 21:21:52,281 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:52,281 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,282 INFO  L256         TraceCheckSpWp]: Trace formula consists of 273 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,284 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,297 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 22 proven. 1 refuted. 0 times theorem prover too weak. 47 trivial. 0 not checked.
[2025-04-28 21:21:52,298 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,502 INFO  L134       CoverageAnalysis]: Checked inductivity of 70 backedges. 22 proven. 1 refuted. 0 times theorem prover too weak. 47 trivial. 0 not checked.
[2025-04-28 21:21:52,502 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1120221670] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,503 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,503 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [4, 4, 4] total 4
[2025-04-28 21:21:52,503 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1356137729]
[2025-04-28 21:21:52,503 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,503 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:52,503 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,504 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:52,504 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:52,504 INFO  L87              Difference]: Start difference. First operand 24 states and 29 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:52,531 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,531 INFO  L93              Difference]: Finished difference Result 26 states and 31 transitions.
[2025-04-28 21:21:52,532 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 3 states. 
[2025-04-28 21:21:52,532 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 33
[2025-04-28 21:21:52,532 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,533 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:52,533 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:52,533 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 71 GetRequests, 66 SyntacticMatches, 2 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:52,533 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 1 mSDsluCounter, 19 mSDsCounter, 0 mSdLazyCounter, 13 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 1 SdHoareTripleChecker+Valid, 35 SdHoareTripleChecker+Invalid, 14 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 13 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,535 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [1 Valid, 35 Invalid, 14 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 13 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:52,535 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:52,540 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:52,540 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 4 states have call successors, (4), 2 states have call predecessors, (4), 9 states have return successors, (13), 9 states have call predecessors, (13), 4 states have call successors, (13)
[2025-04-28 21:21:52,542 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 31 transitions.
[2025-04-28 21:21:52,542 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 31 transitions. Word has length 33
[2025-04-28 21:21:52,542 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,542 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 31 transitions.
[2025-04-28 21:21:52,543 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:52,543 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 31 transitions.
[2025-04-28 21:21:52,543 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:52,543 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,543 INFO  L218           NwaCegarLoop]: trace histogram [7, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,548 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-04-28 21:21:52,744 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,744 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,744 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,745 INFO  L85        PathProgramCache]: Analyzing trace with hash -999795056, now seen corresponding path program 4 times
[2025-04-28 21:21:52,745 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,745 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [208955050]
[2025-04-28 21:21:52,745 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:52,745 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,752 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 33 statements into 2 equivalence classes.
[2025-04-28 21:21:52,765 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:52,765 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:52,765 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,885 INFO  L134       CoverageAnalysis]: Checked inductivity of 73 backedges. 24 proven. 20 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:52,885 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,885 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [208955050]
[2025-04-28 21:21:52,885 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [208955050] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,885 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [422647056]
[2025-04-28 21:21:52,885 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:52,886 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,888 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,890 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,894 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,994 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 33 statements into 2 equivalence classes.
[2025-04-28 21:21:53,047 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:53,047 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:53,047 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,050 INFO  L256         TraceCheckSpWp]: Trace formula consists of 378 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,052 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,085 INFO  L134       CoverageAnalysis]: Checked inductivity of 73 backedges. 24 proven. 20 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:53,086 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,383 INFO  L134       CoverageAnalysis]: Checked inductivity of 73 backedges. 24 proven. 26 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:54,383 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [422647056] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,383 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,383 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 12] total 14
[2025-04-28 21:21:54,384 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1915766103]
[2025-04-28 21:21:54,384 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,384 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:54,384 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,384 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:54,385 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=62, Invalid=120, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:54,385 INFO  L87              Difference]: Start difference. First operand 26 states and 31 transitions. Second operand  has 14 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 14 states have internal predecessors, (18), 8 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (13), 5 states have call predecessors, (13), 8 states have call successors, (13)
[2025-04-28 21:21:54,487 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,487 INFO  L93              Difference]: Finished difference Result 28 states and 33 transitions.
[2025-04-28 21:21:54,487 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:54,487 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 14 states have internal predecessors, (18), 8 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (13), 5 states have call predecessors, (13), 8 states have call successors, (13) Word has length 33
[2025-04-28 21:21:54,488 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,488 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:54,488 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:54,488 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 82 GetRequests, 60 SyntacticMatches, 5 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 58 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=115, Invalid=227, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:54,489 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 15 mSDsluCounter, 30 mSDsCounter, 0 mSdLazyCounter, 40 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 44 SdHoareTripleChecker+Invalid, 58 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 40 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,489 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 44 Invalid, 58 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 40 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:54,489 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:54,491 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 28.
[2025-04-28 21:21:54,492 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 13 states have (on average 1.1538461538461537) internal successors, (15), 15 states have internal predecessors, (15), 4 states have call successors, (4), 2 states have call predecessors, (4), 10 states have return successors, (14), 10 states have call predecessors, (14), 4 states have call successors, (14)
[2025-04-28 21:21:54,492 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 33 transitions.
[2025-04-28 21:21:54,492 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 33 transitions. Word has length 33
[2025-04-28 21:21:54,492 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,492 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 33 transitions.
[2025-04-28 21:21:54,493 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 14 states have internal predecessors, (18), 8 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (13), 5 states have call predecessors, (13), 8 states have call successors, (13)
[2025-04-28 21:21:54,493 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 33 transitions.
[2025-04-28 21:21:54,493 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:54,493 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,493 INFO  L218           NwaCegarLoop]: trace histogram [8, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,499 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Ended with exit code 0
[2025-04-28 21:21:54,694 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable14
[2025-04-28 21:21:54,694 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,694 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,694 INFO  L85        PathProgramCache]: Analyzing trace with hash -481706055, now seen corresponding path program 5 times
[2025-04-28 21:21:54,695 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,695 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [944216271]
[2025-04-28 21:21:54,695 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:54,695 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,701 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 37 statements into 8 equivalence classes.
[2025-04-28 21:21:54,725 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:54,725 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s)
[2025-04-28 21:21:54,725 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,873 INFO  L134       CoverageAnalysis]: Checked inductivity of 99 backedges. 29 proven. 30 refuted. 0 times theorem prover too weak. 40 trivial. 0 not checked.
[2025-04-28 21:21:54,873 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,873 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [944216271]
[2025-04-28 21:21:54,873 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [944216271] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,873 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [806590239]
[2025-04-28 21:21:54,873 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:54,873 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,876 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,878 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:54,882 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,991 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 37 statements into 8 equivalence classes.
[2025-04-28 21:21:55,053 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:55,053 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 8 check-sat command(s)
[2025-04-28 21:21:55,053 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,055 INFO  L256         TraceCheckSpWp]: Trace formula consists of 429 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,057 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,098 INFO  L134       CoverageAnalysis]: Checked inductivity of 99 backedges. 29 proven. 30 refuted. 0 times theorem prover too weak. 40 trivial. 0 not checked.
[2025-04-28 21:21:55,098 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,988 INFO  L134       CoverageAnalysis]: Checked inductivity of 99 backedges. 29 proven. 40 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:56,989 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [806590239] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,989 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,989 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 14] total 16
[2025-04-28 21:21:56,989 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1915870502]
[2025-04-28 21:21:56,989 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,989 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:56,989 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,990 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:56,990 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=80, Invalid=160, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:56,990 INFO  L87              Difference]: Start difference. First operand 28 states and 33 transitions. Second operand  has 16 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 9 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (15), 6 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:21:57,105 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,105 INFO  L93              Difference]: Finished difference Result 30 states and 35 transitions.
[2025-04-28 21:21:57,106 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:57,106 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 9 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (15), 6 states have call predecessors, (15), 9 states have call successors, (15) Word has length 37
[2025-04-28 21:21:57,106 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,106 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:57,107 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:57,107 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 93 GetRequests, 67 SyntacticMatches, 6 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 87 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=155, Invalid=307, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:57,107 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 20 mSDsluCounter, 37 mSDsCounter, 0 mSdLazyCounter, 51 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 27 SdHoareTripleChecker+Valid, 51 SdHoareTripleChecker+Invalid, 72 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 51 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,108 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [27 Valid, 51 Invalid, 72 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 51 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:57,108 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:57,110 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 30.
[2025-04-28 21:21:57,111 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 30 states, 14 states have (on average 1.1428571428571428) internal successors, (16), 16 states have internal predecessors, (16), 4 states have call successors, (4), 2 states have call predecessors, (4), 11 states have return successors, (15), 11 states have call predecessors, (15), 4 states have call successors, (15)
[2025-04-28 21:21:57,111 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 35 transitions.
[2025-04-28 21:21:57,111 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 35 transitions. Word has length 37
[2025-04-28 21:21:57,111 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,112 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 35 transitions.
[2025-04-28 21:21:57,112 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 9 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (15), 6 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:21:57,112 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 35 transitions.
[2025-04-28 21:21:57,112 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:57,113 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,113 INFO  L218           NwaCegarLoop]: trace histogram [9, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,119 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Ended with exit code 0
