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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:39,851 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:39,917 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b6c04e84-dae6-4268-b115-e222130ee53c/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:39,921 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:39,922 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:39,945 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:39,945 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:39,946 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:39,946 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:39,946 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:39,946 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:39,946 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:39,947 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:39,947 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:39,947 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:39,947 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:39,947 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:39,947 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:39,947 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:39,948 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:39,948 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:39,948 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:39,948 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:39,948 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:39,948 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:39,949 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:39,949 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:40,258 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:40,272 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:40,274 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:40,276 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:40,278 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:40,280 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b6c04e84-dae6-4268-b115-e222130ee53c/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-192.smt2
[2025-04-28 21:21:40,281 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:40,288 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:40,464 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b6c04e84-dae6-4268-b115-e222130ee53c/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-192.smt2
[2025-04-28 21:21:40,468 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:40,470 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:40,471 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:40,471 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:40,471 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:40,474 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,495 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40 Unit
[2025-04-28 21:21:40,495 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:40,496 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:40,496 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:40,496 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:40,511 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,511 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,532 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,532 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,534 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,535 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,537 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,539 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,539 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,556 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:40,559 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:40,559 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:40,559 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:40,560 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,563 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,576 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,594 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:40,598 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:40,616 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:40,617 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:40,617 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:40,617 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main8 given in one single declaration
[2025-04-28 21:21:40,617 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main8
[2025-04-28 21:21:40,617 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main8
[2025-04-28 21:21:40,617 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main5 given in one single declaration
[2025-04-28 21:21:40,617 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main5
[2025-04-28 21:21:40,617 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main5
[2025-04-28 21:21:40,618 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main4 given in one single declaration
[2025-04-28 21:21:40,618 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main4
[2025-04-28 21:21:40,618 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main4
[2025-04-28 21:21:40,619 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv_main2 given in one single declaration
[2025-04-28 21:21:40,619 INFO  L130     BoogieDeclarations]: Found specification of procedure inv_main2
[2025-04-28 21:21:40,619 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv_main2
[2025-04-28 21:21:40,619 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:40,619 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:40,619 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:40,677 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:40,679 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:40,805 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:40,805 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:40,821 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:40,822 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:40,822 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:40 BoogieIcfgContainer
[2025-04-28 21:21:40,822 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:40,827 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:40,828 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:40,833 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:40,833 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/3) ...
[2025-04-28 21:21:40,834 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@23e6fca0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:40, skipping insertion in model container
[2025-04-28 21:21:40,834 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (2/3) ...
[2025-04-28 21:21:40,835 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@23e6fca0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:40, skipping insertion in model container
[2025-04-28 21:21:40,835 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:40" (3/3) ...
[2025-04-28 21:21:40,837 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:40,854 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:40,858 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 6 procedures, 25 locations, 35 edges, 6 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:40,921 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:40,948 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;@1c1e9079, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:40,948 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:40,954 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 25 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 5 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:40,962 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:40,962 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,963 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,964 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,971 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,972 INFO  L85        PathProgramCache]: Analyzing trace with hash 303674983, now seen corresponding path program 1 times
[2025-04-28 21:21:40,982 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,983 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2106925594]
[2025-04-28 21:21:40,983 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,985 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,017 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:41,046 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:41,046 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,047 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,527 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:41,528 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,528 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2106925594]
[2025-04-28 21:21:41,529 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2106925594] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,529 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,533 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:41,535 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1291528047]
[2025-04-28 21:21:41,536 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,541 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:41,544 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,580 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:41,582 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:41,584 INFO  L87              Difference]: Start difference. First operand  has 25 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 5 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 7 states have call successors, (7) Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:41,744 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,745 INFO  L93              Difference]: Finished difference Result 29 states and 33 transitions.
[2025-04-28 21:21:41,748 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:41,750 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:41,751 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,760 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:41,760 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:41,765 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:41,770 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 3 mSDsluCounter, 93 mSDsCounter, 0 mSdLazyCounter, 32 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 115 SdHoareTripleChecker+Invalid, 34 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 32 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,775 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 115 Invalid, 34 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 32 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:41,810 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:41,857 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:41,858 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 5 states have call predecessors, (7), 7 states have return successors, (10), 7 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:41,866 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 31 transitions.
[2025-04-28 21:21:41,868 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 31 transitions. Word has length 20
[2025-04-28 21:21:41,869 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,870 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 31 transitions.
[2025-04-28 21:21:41,871 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 4 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:41,871 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 31 transitions.
[2025-04-28 21:21:41,872 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:41,873 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,873 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,873 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:41,873 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,875 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,876 INFO  L85        PathProgramCache]: Analyzing trace with hash 1414420255, now seen corresponding path program 1 times
[2025-04-28 21:21:41,876 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,876 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1828430765]
[2025-04-28 21:21:41,876 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,876 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,889 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:41,899 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:41,899 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,899 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,140 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:42,141 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,141 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1828430765]
[2025-04-28 21:21:42,141 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1828430765] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,141 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,141 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:42,141 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [989523355]
[2025-04-28 21:21:42,141 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,143 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:42,143 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,144 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:42,146 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,147 INFO  L87              Difference]: Start difference. First operand 27 states and 31 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:42,247 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,247 INFO  L93              Difference]: Finished difference Result 29 states and 33 transitions.
[2025-04-28 21:21:42,249 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:42,249 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6) Word has length 24
[2025-04-28 21:21:42,250 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,250 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:42,250 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:42,251 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:42,252 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 3 mSDsluCounter, 78 mSDsCounter, 0 mSdLazyCounter, 32 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 101 SdHoareTripleChecker+Invalid, 33 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 32 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,255 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 101 Invalid, 33 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 32 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:42,256 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:42,262 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 25.
[2025-04-28 21:21:42,262 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 25 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 13 states have internal predecessors, (13), 7 states have call successors, (7), 5 states have call predecessors, (7), 6 states have return successors, (8), 6 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:42,263 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 28 transitions.
[2025-04-28 21:21:42,265 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 28 transitions. Word has length 24
[2025-04-28 21:21:42,265 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,265 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 28 transitions.
[2025-04-28 21:21:42,265 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:42,266 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 28 transitions.
[2025-04-28 21:21:42,266 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:42,267 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,267 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,267 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:42,267 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,267 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,268 INFO  L85        PathProgramCache]: Analyzing trace with hash 781918934, now seen corresponding path program 1 times
[2025-04-28 21:21:42,268 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,268 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1227337039]
[2025-04-28 21:21:42,268 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,268 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,277 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:42,285 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:42,286 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,286 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,500 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:42,500 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,501 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1227337039]
[2025-04-28 21:21:42,501 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1227337039] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,502 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [313882887]
[2025-04-28 21:21:42,503 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,503 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,505 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,511 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:42,512 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,558 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:42,582 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:42,582 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,582 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,589 INFO  L256         TraceCheckSpWp]: Trace formula consists of 86 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,598 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,849 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:42,850 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,686 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:43,687 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [313882887] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,687 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,687 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 14
[2025-04-28 21:21:43,687 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [511168914]
[2025-04-28 21:21:43,688 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,688 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:43,689 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,691 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:43,692 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=33, Invalid=149, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:43,692 INFO  L87              Difference]: Start difference. First operand 25 states and 28 transitions. Second operand  has 14 states, 10 states have (on average 1.9) internal successors, (19), 14 states have internal predecessors, (19), 7 states have call successors, (9), 1 states have call predecessors, (9), 10 states have return successors, (13), 9 states have call predecessors, (13), 7 states have call successors, (13)
[2025-04-28 21:21:43,867 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,867 INFO  L93              Difference]: Finished difference Result 31 states and 35 transitions.
[2025-04-28 21:21:43,869 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:43,869 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 10 states have (on average 1.9) internal successors, (19), 14 states have internal predecessors, (19), 7 states have call successors, (9), 1 states have call predecessors, (9), 10 states have return successors, (13), 9 states have call predecessors, (13), 7 states have call successors, (13) Word has length 24
[2025-04-28 21:21:43,870 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,871 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:43,872 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:21:43,873 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 43 SyntacticMatches, 0 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 19 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=39, Invalid=171, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:43,875 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 5 mSDsluCounter, 137 mSDsCounter, 0 mSdLazyCounter, 60 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 160 SdHoareTripleChecker+Invalid, 63 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 60 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,876 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 160 Invalid, 63 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 60 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:43,877 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:21:43,885 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:21:43,886 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 13 states have (on average 1.1538461538461537) internal successors, (15), 15 states have internal predecessors, (15), 7 states have call successors, (7), 5 states have call predecessors, (7), 8 states have return successors, (11), 8 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:43,888 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 33 transitions.
[2025-04-28 21:21:43,888 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 33 transitions. Word has length 24
[2025-04-28 21:21:43,888 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,889 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 33 transitions.
[2025-04-28 21:21:43,889 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 10 states have (on average 1.9) internal successors, (19), 14 states have internal predecessors, (19), 7 states have call successors, (9), 1 states have call predecessors, (9), 10 states have return successors, (13), 9 states have call predecessors, (13), 7 states have call successors, (13)
[2025-04-28 21:21:43,890 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 33 transitions.
[2025-04-28 21:21:43,890 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:43,890 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,890 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,898 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:44,091 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,091 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,092 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,092 INFO  L85        PathProgramCache]: Analyzing trace with hash 236299854, now seen corresponding path program 1 times
[2025-04-28 21:21:44,093 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,093 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [857071435]
[2025-04-28 21:21:44,093 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,093 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,102 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:44,112 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:44,112 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,113 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,279 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:44,280 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,280 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [857071435]
[2025-04-28 21:21:44,280 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [857071435] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:44,280 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2143231559]
[2025-04-28 21:21:44,280 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,280 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,284 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,286 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:44,289 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,329 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:44,347 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:44,348 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,348 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,349 INFO  L256         TraceCheckSpWp]: Trace formula consists of 105 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,351 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,415 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:44,416 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,817 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:45,817 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2143231559] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,817 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,818 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:45,818 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1874842294]
[2025-04-28 21:21:45,818 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,818 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:45,818 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,819 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:45,819 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=33, Invalid=99, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:45,819 INFO  L87              Difference]: Start difference. First operand 29 states and 33 transitions. Second operand  has 12 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 12 states have internal predecessors, (19), 8 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 6 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:45,934 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,934 INFO  L93              Difference]: Finished difference Result 31 states and 35 transitions.
[2025-04-28 21:21:45,936 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:45,936 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 12 states have internal predecessors, (19), 8 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 6 states have call predecessors, (10), 8 states have call successors, (10) Word has length 28
[2025-04-28 21:21:45,936 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,937 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:45,937 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:21:45,937 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 50 SyntacticMatches, 3 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 14 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=49, Invalid=161, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:45,938 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 7 mSDsluCounter, 79 mSDsCounter, 0 mSdLazyCounter, 45 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 103 SdHoareTripleChecker+Invalid, 50 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 45 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,938 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 103 Invalid, 50 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 45 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,939 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:21:45,946 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 27.
[2025-04-28 21:21:45,946 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 7 states have call successors, (7), 5 states have call predecessors, (7), 7 states have return successors, (9), 7 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:45,948 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 30 transitions.
[2025-04-28 21:21:45,949 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 30 transitions. Word has length 28
[2025-04-28 21:21:45,950 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,950 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 30 transitions.
[2025-04-28 21:21:45,951 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 12 states have internal predecessors, (19), 8 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (10), 6 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:45,951 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 30 transitions.
[2025-04-28 21:21:45,951 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:45,952 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,952 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,958 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:46,152 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,152 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,153 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,153 INFO  L85        PathProgramCache]: Analyzing trace with hash 993879301, now seen corresponding path program 2 times
[2025-04-28 21:21:46,153 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,153 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [960391903]
[2025-04-28 21:21:46,153 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,153 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,159 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:46,166 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:46,166 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:46,166 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,294 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:46,295 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,295 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [960391903]
[2025-04-28 21:21:46,295 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [960391903] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,295 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1580193320]
[2025-04-28 21:21:46,295 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,295 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,298 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,300 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:46,303 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,351 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:46,371 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:46,371 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:46,371 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,372 INFO  L256         TraceCheckSpWp]: Trace formula consists of 105 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,374 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,429 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:46,429 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,942 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 6 proven. 1 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:47,943 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1580193320] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,943 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,943 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 9] total 14
[2025-04-28 21:21:47,943 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1114742802]
[2025-04-28 21:21:47,943 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,944 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:47,944 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,944 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:47,945 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=142, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:47,945 INFO  L87              Difference]: Start difference. First operand 27 states and 30 transitions. Second operand  has 14 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 14 states have internal predecessors, (21), 9 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (12), 8 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:48,067 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,067 INFO  L93              Difference]: Finished difference Result 29 states and 32 transitions.
[2025-04-28 21:21:48,069 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:48,070 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 14 states have internal predecessors, (21), 9 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (12), 8 states have call predecessors, (12), 9 states have call successors, (12) Word has length 28
[2025-04-28 21:21:48,070 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,070 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:48,071 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:21:48,071 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 67 GetRequests, 48 SyntacticMatches, 4 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=70, Invalid=202, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:48,072 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 4 mSDsluCounter, 125 mSDsCounter, 0 mSdLazyCounter, 61 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 149 SdHoareTripleChecker+Invalid, 66 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 61 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,072 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 149 Invalid, 66 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 61 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:48,075 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:21:48,079 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:21:48,081 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 13 states have (on average 1.1538461538461537) internal successors, (15), 15 states have internal predecessors, (15), 7 states have call successors, (7), 5 states have call predecessors, (7), 8 states have return successors, (10), 8 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:48,084 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 32 transitions.
[2025-04-28 21:21:48,084 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 32 transitions. Word has length 28
[2025-04-28 21:21:48,085 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,085 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 32 transitions.
[2025-04-28 21:21:48,085 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 14 states have internal predecessors, (21), 9 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (12), 8 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:48,085 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 32 transitions.
[2025-04-28 21:21:48,086 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:48,086 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,086 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,092 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:48,286 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,287 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,287 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,287 INFO  L85        PathProgramCache]: Analyzing trace with hash 1287265085, now seen corresponding path program 2 times
[2025-04-28 21:21:48,288 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,288 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1369666247]
[2025-04-28 21:21:48,288 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:48,288 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,297 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:21:48,304 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:48,304 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,304 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,587 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:48,587 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,588 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1369666247]
[2025-04-28 21:21:48,588 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1369666247] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:48,588 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [756344712]
[2025-04-28 21:21:48,588 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:48,588 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:48,594 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:48,596 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:48,601 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:48,673 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:21:48,695 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:48,695 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,695 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,697 INFO  L256         TraceCheckSpWp]: Trace formula consists of 124 conjuncts, 35 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,699 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,924 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:48,924 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,023 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 9 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:50,023 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [756344712] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,023 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,023 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 12] total 21
[2025-04-28 21:21:50,023 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [754060185]
[2025-04-28 21:21:50,023 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,024 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:50,024 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,025 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:50,025 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=55, Invalid=365, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:50,025 INFO  L87              Difference]: Start difference. First operand 29 states and 32 transitions. Second operand  has 21 states, 14 states have (on average 1.8571428571428572) internal successors, (26), 21 states have internal predecessors, (26), 10 states have call successors, (12), 1 states have call predecessors, (12), 14 states have return successors, (19), 13 states have call predecessors, (19), 10 states have call successors, (19)
[2025-04-28 21:21:50,236 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,236 INFO  L93              Difference]: Finished difference Result 37 states and 41 transitions.
[2025-04-28 21:21:50,237 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:50,237 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 14 states have (on average 1.8571428571428572) internal successors, (26), 21 states have internal predecessors, (26), 10 states have call successors, (12), 1 states have call predecessors, (12), 14 states have return successors, (19), 13 states have call predecessors, (19), 10 states have call successors, (19) Word has length 32
[2025-04-28 21:21:50,237 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,238 INFO  L225             Difference]: With dead ends: 37
[2025-04-28 21:21:50,238 INFO  L226             Difference]: Without dead ends: 35
[2025-04-28 21:21:50,239 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 78 GetRequests, 56 SyntacticMatches, 0 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 66 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=75, Invalid=477, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:50,241 INFO  L437           NwaCegarLoop]: 25 mSDtfsCounter, 9 mSDsluCounter, 240 mSDsCounter, 0 mSdLazyCounter, 138 mSolverCounterSat, 4 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 265 SdHoareTripleChecker+Invalid, 142 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 4 IncrementalHoareTripleChecker+Valid, 138 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,241 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 265 Invalid, 142 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [4 Valid, 138 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:50,244 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 35 states.
[2025-04-28 21:21:50,247 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 35 to 33.
[2025-04-28 21:21:50,247 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 15 states have (on average 1.1333333333333333) internal successors, (17), 17 states have internal predecessors, (17), 7 states have call successors, (7), 5 states have call predecessors, (7), 10 states have return successors, (13), 10 states have call predecessors, (13), 7 states have call successors, (13)
[2025-04-28 21:21:50,248 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 37 transitions.
[2025-04-28 21:21:50,248 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 37 transitions. Word has length 32
[2025-04-28 21:21:50,248 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,249 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 37 transitions.
[2025-04-28 21:21:50,249 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 14 states have (on average 1.8571428571428572) internal successors, (26), 21 states have internal predecessors, (26), 10 states have call successors, (12), 1 states have call predecessors, (12), 14 states have return successors, (19), 13 states have call predecessors, (19), 10 states have call successors, (19)
[2025-04-28 21:21:50,249 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 37 transitions.
[2025-04-28 21:21:50,250 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:50,250 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,250 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,256 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:50,455 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,455 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,456 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,456 INFO  L85        PathProgramCache]: Analyzing trace with hash 296150517, now seen corresponding path program 3 times
[2025-04-28 21:21:50,456 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,456 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1347702190]
[2025-04-28 21:21:50,456 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:50,456 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,470 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 36 statements into 3 equivalence classes.
[2025-04-28 21:21:50,485 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:50,485 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:50,485 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,728 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 7 proven. 7 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:50,729 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,729 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1347702190]
[2025-04-28 21:21:50,729 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1347702190] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,729 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1448415572]
[2025-04-28 21:21:50,729 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:50,729 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,732 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,735 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:50,739 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,811 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 36 statements into 3 equivalence classes.
[2025-04-28 21:21:50,834 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:50,834 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 3 check-sat command(s)
[2025-04-28 21:21:50,834 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,837 INFO  L256         TraceCheckSpWp]: Trace formula consists of 143 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,839 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,945 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 6 proven. 7 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:50,945 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,764 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 6 proven. 8 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:53,765 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1448415572] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,765 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,765 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 12] total 21
[2025-04-28 21:21:53,765 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1797765687]
[2025-04-28 21:21:53,765 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,765 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:53,766 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,766 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:53,767 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=82, Invalid=338, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:53,767 INFO  L87              Difference]: Start difference. First operand 33 states and 37 transitions. Second operand  has 21 states, 11 states have (on average 2.6363636363636362) internal successors, (29), 21 states have internal predecessors, (29), 14 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (17), 10 states have call predecessors, (17), 14 states have call successors, (17)
[2025-04-28 21:21:54,016 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,016 INFO  L93              Difference]: Finished difference Result 35 states and 38 transitions.
[2025-04-28 21:21:54,017 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:54,017 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 11 states have (on average 2.6363636363636362) internal successors, (29), 21 states have internal predecessors, (29), 14 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (17), 10 states have call predecessors, (17), 14 states have call successors, (17) Word has length 36
[2025-04-28 21:21:54,018 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,018 INFO  L225             Difference]: With dead ends: 35
[2025-04-28 21:21:54,018 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:54,019 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 89 GetRequests, 60 SyntacticMatches, 4 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 131 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=134, Invalid=568, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:54,020 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 14 mSDsluCounter, 201 mSDsCounter, 0 mSdLazyCounter, 96 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 225 SdHoareTripleChecker+Invalid, 108 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 96 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,020 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 225 Invalid, 108 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 96 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:54,021 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:54,024 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 31.
[2025-04-28 21:21:54,024 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 14 states have (on average 1.1428571428571428) internal successors, (16), 16 states have internal predecessors, (16), 7 states have call successors, (7), 5 states have call predecessors, (7), 9 states have return successors, (11), 9 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:54,025 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 34 transitions.
[2025-04-28 21:21:54,026 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 34 transitions. Word has length 36
[2025-04-28 21:21:54,026 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,026 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 34 transitions.
[2025-04-28 21:21:54,026 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 11 states have (on average 2.6363636363636362) internal successors, (29), 21 states have internal predecessors, (29), 14 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (17), 10 states have call predecessors, (17), 14 states have call successors, (17)
[2025-04-28 21:21:54,026 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 34 transitions.
[2025-04-28 21:21:54,027 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:54,027 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,027 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,035 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:54,232 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,232 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,232 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,232 INFO  L85        PathProgramCache]: Analyzing trace with hash 1702004204, now seen corresponding path program 4 times
[2025-04-28 21:21:54,233 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,233 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1469792489]
[2025-04-28 21:21:54,233 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:54,233 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,242 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 36 statements into 2 equivalence classes.
[2025-04-28 21:21:54,250 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:54,250 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:54,250 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,462 INFO  L134       CoverageAnalysis]: Checked inductivity of 24 backedges. 6 proven. 10 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:54,462 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,462 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1469792489]
[2025-04-28 21:21:54,462 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1469792489] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,462 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [820165130]
[2025-04-28 21:21:54,462 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:54,462 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,466 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,468 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:54,472 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,562 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 36 statements into 2 equivalence classes.
[2025-04-28 21:21:54,581 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:54,581 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:54,582 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,583 INFO  L256         TraceCheckSpWp]: Trace formula consists of 143 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,584 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,634 INFO  L134       CoverageAnalysis]: Checked inductivity of 24 backedges. 6 proven. 10 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:54,634 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:57,585 INFO  L134       CoverageAnalysis]: Checked inductivity of 24 backedges. 12 proven. 5 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:57,585 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [820165130] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:57,586 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:57,586 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 13] total 19
[2025-04-28 21:21:57,586 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [86631967]
[2025-04-28 21:21:57,586 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,586 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:57,587 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,587 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:57,587 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=66, Invalid=276, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:57,588 INFO  L87              Difference]: Start difference. First operand 31 states and 34 transitions. Second operand  has 19 states, 11 states have (on average 2.272727272727273) internal successors, (25), 19 states have internal predecessors, (25), 11 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (14), 10 states have call predecessors, (14), 11 states have call successors, (14)
[2025-04-28 21:21:57,765 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,766 INFO  L93              Difference]: Finished difference Result 33 states and 36 transitions.
[2025-04-28 21:21:57,766 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:57,766 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 11 states have (on average 2.272727272727273) internal successors, (25), 19 states have internal predecessors, (25), 11 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (14), 10 states have call predecessors, (14), 11 states have call successors, (14) Word has length 36
[2025-04-28 21:21:57,767 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,767 INFO  L225             Difference]: With dead ends: 33
[2025-04-28 21:21:57,767 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:21:57,768 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 89 GetRequests, 62 SyntacticMatches, 5 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 62 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=122, Invalid=430, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:57,769 INFO  L437           NwaCegarLoop]: 25 mSDtfsCounter, 7 mSDsluCounter, 174 mSDsCounter, 0 mSdLazyCounter, 118 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 199 SdHoareTripleChecker+Invalid, 123 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 118 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,769 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 199 Invalid, 123 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 118 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:57,769 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:21:57,773 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 33.
[2025-04-28 21:21:57,773 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 15 states have (on average 1.1333333333333333) internal successors, (17), 17 states have internal predecessors, (17), 7 states have call successors, (7), 5 states have call predecessors, (7), 10 states have return successors, (12), 10 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:57,774 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 36 transitions.
[2025-04-28 21:21:57,774 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 36 transitions. Word has length 36
[2025-04-28 21:21:57,775 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,775 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 36 transitions.
[2025-04-28 21:21:57,775 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 11 states have (on average 2.272727272727273) internal successors, (25), 19 states have internal predecessors, (25), 11 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (14), 10 states have call predecessors, (14), 11 states have call successors, (14)
[2025-04-28 21:21:57,775 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 36 transitions.
[2025-04-28 21:21:57,776 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:57,776 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,776 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,782 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:57,977 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,977 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,977 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,978 INFO  L85        PathProgramCache]: Analyzing trace with hash 814670692, now seen corresponding path program 5 times
[2025-04-28 21:21:57,978 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,978 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2079938757]
[2025-04-28 21:21:57,978 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:57,978 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,983 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 40 statements into 4 equivalence classes.
[2025-04-28 21:21:57,991 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:57,991 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s)
[2025-04-28 21:21:57,991 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,341 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 18 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:58,341 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,341 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2079938757]
[2025-04-28 21:21:58,341 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2079938757] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,341 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1992437657]
[2025-04-28 21:21:58,341 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:58,342 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,345 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:58,347 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:58,352 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,485 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 40 statements into 4 equivalence classes.
[2025-04-28 21:21:58,513 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:58,513 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 4 check-sat command(s)
[2025-04-28 21:21:58,513 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,516 INFO  L256         TraceCheckSpWp]: Trace formula consists of 162 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,519 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,692 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 18 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:58,692 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:00,169 INFO  L134       CoverageAnalysis]: Checked inductivity of 31 backedges. 0 proven. 22 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:22:00,169 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1992437657] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:00,169 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:00,169 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 16] total 22
[2025-04-28 21:22:00,169 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [8251080]
[2025-04-28 21:22:00,170 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,170 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:00,170 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,171 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:00,171 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=57, Invalid=405, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:00,171 INFO  L87              Difference]: Start difference. First operand 33 states and 36 transitions. Second operand  has 22 states, 13 states have (on average 2.0) internal successors, (26), 22 states have internal predecessors, (26), 11 states have call successors, (13), 1 states have call predecessors, (13), 13 states have return successors, (20), 12 states have call predecessors, (20), 11 states have call successors, (20)
[2025-04-28 21:22:00,418 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,418 INFO  L93              Difference]: Finished difference Result 43 states and 47 transitions.
[2025-04-28 21:22:00,419 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:00,419 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 13 states have (on average 2.0) internal successors, (26), 22 states have internal predecessors, (26), 11 states have call successors, (13), 1 states have call predecessors, (13), 13 states have return successors, (20), 12 states have call predecessors, (20), 11 states have call successors, (20) Word has length 40
[2025-04-28 21:22:00,420 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:00,420 INFO  L225             Difference]: With dead ends: 43
[2025-04-28 21:22:00,420 INFO  L226             Difference]: Without dead ends: 41
[2025-04-28 21:22:00,421 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 100 GetRequests, 75 SyntacticMatches, 0 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 61 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=92, Invalid=610, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:00,421 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 12 mSDsluCounter, 271 mSDsCounter, 0 mSdLazyCounter, 165 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 298 SdHoareTripleChecker+Invalid, 170 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 165 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:00,422 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 298 Invalid, 170 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 165 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:00,422 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 41 states.
[2025-04-28 21:22:00,426 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 41 to 37.
[2025-04-28 21:22:00,426 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 37 states, 17 states have (on average 1.1176470588235294) internal successors, (19), 19 states have internal predecessors, (19), 7 states have call successors, (7), 5 states have call predecessors, (7), 12 states have return successors, (15), 12 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:22:00,427 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 37 states to 37 states and 41 transitions.
[2025-04-28 21:22:00,427 INFO  L79                 Accepts]: Start accepts. Automaton has 37 states and 41 transitions. Word has length 40
[2025-04-28 21:22:00,427 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:00,427 INFO  L485      AbstractCegarLoop]: Abstraction has 37 states and 41 transitions.
[2025-04-28 21:22:00,427 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 13 states have (on average 2.0) internal successors, (26), 22 states have internal predecessors, (26), 11 states have call successors, (13), 1 states have call predecessors, (13), 13 states have return successors, (20), 12 states have call predecessors, (20), 11 states have call successors, (20)
[2025-04-28 21:22:00,427 INFO  L278                IsEmpty]: Start isEmpty. Operand 37 states and 41 transitions.
[2025-04-28 21:22:00,428 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:22:00,428 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:00,429 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:00,435 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:00,633 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:00,633 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,633 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,633 INFO  L85        PathProgramCache]: Analyzing trace with hash -1970407789, now seen corresponding path program 6 times
[2025-04-28 21:22:00,633 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,633 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1467197016]
[2025-04-28 21:22:00,633 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:22:00,634 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,640 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 44 statements into 5 equivalence classes.
[2025-04-28 21:22:00,648 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 5 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:22:00,649 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 5 check-sat command(s)
[2025-04-28 21:22:00,649 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,934 INFO  L134       CoverageAnalysis]: Checked inductivity of 46 backedges. 8 proven. 24 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:00,934 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,934 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1467197016]
[2025-04-28 21:22:00,934 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1467197016] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,934 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1031269894]
[2025-04-28 21:22:00,934 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:22:00,934 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,936 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,938 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:00,941 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:22:01,064 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 44 statements into 5 equivalence classes.
[2025-04-28 21:22:01,092 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 5 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:22:01,092 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 5 check-sat command(s)
[2025-04-28 21:22:01,092 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,094 INFO  L256         TraceCheckSpWp]: Trace formula consists of 181 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:01,096 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:01,189 INFO  L134       CoverageAnalysis]: Checked inductivity of 46 backedges. 12 proven. 17 refuted. 0 times theorem prover too weak. 17 trivial. 0 not checked.
[2025-04-28 21:22:01,190 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:08,026 INFO  L134       CoverageAnalysis]: Checked inductivity of 46 backedges. 20 proven. 13 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:22:08,026 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1031269894] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,026 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,026 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 14, 17] total 27
[2025-04-28 21:22:08,026 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [565486775]
[2025-04-28 21:22:08,027 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,027 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:22:08,027 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,028 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:22:08,028 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=116, Invalid=586, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:08,028 INFO  L87              Difference]: Start difference. First operand 37 states and 41 transitions. Second operand  has 27 states, 15 states have (on average 2.2666666666666666) internal successors, (34), 27 states have internal predecessors, (34), 16 states have call successors, (18), 1 states have call predecessors, (18), 15 states have return successors, (22), 14 states have call predecessors, (22), 16 states have call successors, (22)
[2025-04-28 21:22:08,323 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:08,323 INFO  L93              Difference]: Finished difference Result 43 states and 47 transitions.
[2025-04-28 21:22:08,323 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:22:08,324 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 15 states have (on average 2.2666666666666666) internal successors, (34), 27 states have internal predecessors, (34), 16 states have call successors, (18), 1 states have call predecessors, (18), 15 states have return successors, (22), 14 states have call predecessors, (22), 16 states have call successors, (22) Word has length 44
[2025-04-28 21:22:08,324 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,325 INFO  L225             Difference]: With dead ends: 43
[2025-04-28 21:22:08,326 INFO  L226             Difference]: Without dead ends: 43
[2025-04-28 21:22:08,326 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 111 GetRequests, 73 SyntacticMatches, 6 SemanticMatches, 32 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 190 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=214, Invalid=908, Unknown=0, NotChecked=0, Total=1122
[2025-04-28 21:22:08,330 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 10 mSDsluCounter, 300 mSDsCounter, 0 mSdLazyCounter, 221 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 328 SdHoareTripleChecker+Invalid, 236 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 221 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,330 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 328 Invalid, 236 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 221 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:08,331 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 43 states.
[2025-04-28 21:22:08,334 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 43 to 35.
[2025-04-28 21:22:08,334 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 16 states have (on average 1.125) internal successors, (18), 18 states have internal predecessors, (18), 7 states have call successors, (7), 5 states have call predecessors, (7), 11 states have return successors, (13), 11 states have call predecessors, (13), 7 states have call successors, (13)
[2025-04-28 21:22:08,335 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 38 transitions.
[2025-04-28 21:22:08,335 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 38 transitions. Word has length 44
[2025-04-28 21:22:08,336 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,336 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 38 transitions.
[2025-04-28 21:22:08,336 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 15 states have (on average 2.2666666666666666) internal successors, (34), 27 states have internal predecessors, (34), 16 states have call successors, (18), 1 states have call predecessors, (18), 15 states have return successors, (22), 14 states have call predecessors, (22), 16 states have call successors, (22)
[2025-04-28 21:22:08,336 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 38 transitions.
[2025-04-28 21:22:08,337 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:22:08,337 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,337 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 3, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:08,342 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:22:08,541 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:08,541 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:08,541 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:08,541 INFO  L85        PathProgramCache]: Analyzing trace with hash -1071381156, now seen corresponding path program 7 times
[2025-04-28 21:22:08,542 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:08,542 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1792554020]
[2025-04-28 21:22:08,542 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:08,542 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:08,549 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:22:08,556 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:22:08,556 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:08,556 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,771 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 12 proven. 14 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:22:08,771 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:08,772 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1792554020]
[2025-04-28 21:22:08,772 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1792554020] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:08,772 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [827699291]
[2025-04-28 21:22:08,772 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:08,772 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:08,774 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:08,777 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:08,794 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:09,034 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:22:09,065 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:22:09,066 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:09,066 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,067 INFO  L256         TraceCheckSpWp]: Trace formula consists of 181 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:09,070 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:09,135 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 12 proven. 14 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:22:09,135 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
