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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:26,601 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:26,696 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a612c329-3c06-46a4-8582-435a7b54d902/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:26,703 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:26,704 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:26,738 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:26,739 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:26,739 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:26,739 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:26,739 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:26,740 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:26,740 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:26,740 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:26,740 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:26,740 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:26,740 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:26,741 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:26,742 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:26,742 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:26,743 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:26,743 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:26,743 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:26,743 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:26,743 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:26,743 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:26,744 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:26,745 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:27,074 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:27,085 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:27,088 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:27,091 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:27,091 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:27,092 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a612c329-3c06-46a4-8582-435a7b54d902/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-019.smt2
[2025-04-28 21:21:27,093 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:27,099 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:27,302 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a612c329-3c06-46a4-8582-435a7b54d902/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-019.smt2
[2025-04-28 21:21:27,305 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:27,309 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:27,310 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:27,310 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:27,310 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:27,313 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,349 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27 Unit
[2025-04-28 21:21:27,350 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:27,351 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:27,353 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:27,353 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:27,370 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,370 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,395 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,396 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,400 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,404 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,406 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,410 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,411 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,423 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:27,424 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:27,424 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:27,424 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:27,425 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (1/1) ...
[2025-04-28 21:21:27,428 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:27,447 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,464 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:27,473 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:27,486 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:27,486 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:27,486 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:27,486 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATverifier.error.split given in one single declaration
[2025-04-28 21:21:27,486 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATverifier.error.split
[2025-04-28 21:21:27,486 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATverifier.error.split
[2025-04-28 21:21:27,486 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibonacci given in one single declaration
[2025-04-28 21:21:27,486 INFO  L130     BoogieDeclarations]: Found specification of procedure fibonacci
[2025-04-28 21:21:27,486 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibonacci
[2025-04-28 21:21:27,487 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibonacci.AT.split given in one single declaration
[2025-04-28 21:21:27,487 INFO  L130     BoogieDeclarations]: Found specification of procedure fibonacci.AT.split
[2025-04-28 21:21:27,487 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibonacci.AT.split
[2025-04-28 21:21:27,487 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fibonacci.AT_call given in one single declaration
[2025-04-28 21:21:27,487 INFO  L130     BoogieDeclarations]: Found specification of procedure fibonacci.AT_call
[2025-04-28 21:21:27,487 INFO  L138     BoogieDeclarations]: Found implementation of procedure fibonacci.AT_call
[2025-04-28 21:21:27,487 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:27,487 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:27,487 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:27,488 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:27,488 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:27,488 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:27,541 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:27,544 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:27,713 INFO  L?                        ?]: Removed 21 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:27,713 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:27,733 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:27,734 INFO  L312             CfgBuilder]: Removed 3 assume(true) statements.
[2025-04-28 21:21:27,735 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:27 BoogieIcfgContainer
[2025-04-28 21:21:27,735 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:27,739 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:27,740 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:27,744 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:27,745 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:27" (1/3) ...
[2025-04-28 21:21:27,746 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7fdb389d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:27, skipping insertion in model container
[2025-04-28 21:21:27,747 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:27" (2/3) ...
[2025-04-28 21:21:27,747 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@7fdb389d and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:27, skipping insertion in model container
[2025-04-28 21:21:27,747 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:27" (3/3) ...
[2025-04-28 21:21:27,749 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:27,760 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:27,763 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 27 locations, 39 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:27,806 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:27,818 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;@3e3c556e, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:27,818 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:27,822 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 27 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 6 states have call predecessors, (8), 6 states have return successors, (8), 8 states have call predecessors, (8), 8 states have call successors, (8)
[2025-04-28 21:21:27,833 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:27,834 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,836 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,837 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,842 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,843 INFO  L85        PathProgramCache]: Analyzing trace with hash -551916616, now seen corresponding path program 1 times
[2025-04-28 21:21:27,851 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,852 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [25797686]
[2025-04-28 21:21:27,852 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,856 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,892 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:27,915 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:27,915 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,915 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,049 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:28,049 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,050 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [25797686]
[2025-04-28 21:21:28,050 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [25797686] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,050 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,053 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:28,055 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1911320928]
[2025-04-28 21:21:28,055 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,059 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:28,060 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,084 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:28,085 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,087 INFO  L87              Difference]: Start difference. First operand  has 27 states, 11 states have (on average 1.3636363636363635) internal successors, (15), 13 states have internal predecessors, (15), 8 states have call successors, (8), 6 states have call predecessors, (8), 6 states have return successors, (8), 8 states have call predecessors, (8), 8 states have call successors, (8) Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:28,142 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,143 INFO  L93              Difference]: Finished difference Result 27 states and 32 transitions.
[2025-04-28 21:21:28,148 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:28,149 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 15
[2025-04-28 21:21:28,149 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,155 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:28,155 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:28,157 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,160 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 1 mSDsluCounter, 43 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 70 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,161 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 70 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:28,175 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:28,193 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:28,194 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 13 states have internal predecessors, (14), 8 states have call successors, (8), 6 states have call predecessors, (8), 7 states have return successors, (10), 8 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:28,197 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:28,199 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:28,199 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,202 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:28,203 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:28,203 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:28,204 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 16
[2025-04-28 21:21:28,204 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,204 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,205 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:28,205 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,205 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,205 INFO  L85        PathProgramCache]: Analyzing trace with hash -1609497408, now seen corresponding path program 1 times
[2025-04-28 21:21:28,205 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,206 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1828116728]
[2025-04-28 21:21:28,206 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,206 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,212 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 15 statements into 1 equivalence classes.
[2025-04-28 21:21:28,219 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 15 of 15 statements.
[2025-04-28 21:21:28,219 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,219 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,360 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:28,360 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,360 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1828116728]
[2025-04-28 21:21:28,360 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1828116728] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,360 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,360 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:28,361 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [629736022]
[2025-04-28 21:21:28,361 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,362 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:28,362 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,363 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:28,364 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,364 INFO  L87              Difference]: Start difference. First operand 27 states and 32 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:28,413 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,415 INFO  L93              Difference]: Finished difference Result 31 states and 38 transitions.
[2025-04-28 21:21:28,416 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:28,416 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 15
[2025-04-28 21:21:28,416 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,417 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:21:28,418 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:21:28,419 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,420 INFO  L437           NwaCegarLoop]: 27 mSDtfsCounter, 1 mSDsluCounter, 43 mSDsCounter, 0 mSdLazyCounter, 11 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 70 SdHoareTripleChecker+Invalid, 12 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 11 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,424 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 70 Invalid, 12 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 11 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:28,425 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:21:28,431 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 27.
[2025-04-28 21:21:28,432 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.2727272727272727) internal successors, (14), 12 states have internal predecessors, (14), 8 states have call successors, (8), 6 states have call predecessors, (8), 7 states have return successors, (10), 8 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:28,435 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 32 transitions.
[2025-04-28 21:21:28,435 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 32 transitions. Word has length 15
[2025-04-28 21:21:28,435 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,435 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 32 transitions.
[2025-04-28 21:21:28,436 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:28,436 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 32 transitions.
[2025-04-28 21:21:28,437 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:28,439 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,439 INFO  L218           NwaCegarLoop]: trace histogram [3, 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, 1]
[2025-04-28 21:21:28,439 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:28,440 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,440 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,441 INFO  L85        PathProgramCache]: Analyzing trace with hash 115978980, now seen corresponding path program 1 times
[2025-04-28 21:21:28,441 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,441 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1781532448]
[2025-04-28 21:21:28,441 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,441 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,452 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:28,461 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:28,462 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,462 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,532 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:28,532 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,532 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1781532448]
[2025-04-28 21:21:28,532 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1781532448] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,532 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [850388989]
[2025-04-28 21:21:28,533 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,533 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,535 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,538 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:28,542 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,604 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:28,645 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:28,645 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,645 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,648 INFO  L256         TraceCheckSpWp]: Trace formula consists of 115 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,655 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,746 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:28,747 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:28,747 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [850388989] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,747 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:28,747 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 5
[2025-04-28 21:21:28,747 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [922228485]
[2025-04-28 21:21:28,748 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,748 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:28,748 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,749 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:28,749 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:28,750 INFO  L87              Difference]: Start difference. First operand 27 states and 32 transitions. Second operand  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:28,788 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,789 INFO  L93              Difference]: Finished difference Result 29 states and 34 transitions.
[2025-04-28 21:21:28,792 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:28,793 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:28,793 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,794 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:28,794 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:21:28,794 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 30 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:28,795 INFO  L437           NwaCegarLoop]: 28 mSDtfsCounter, 1 mSDsluCounter, 45 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 73 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,795 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 73 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:28,796 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:21:28,801 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:21:28,802 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 12 states have (on average 1.25) internal successors, (15), 14 states have internal predecessors, (15), 8 states have call successors, (8), 6 states have call predecessors, (8), 8 states have return successors, (11), 8 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:28,806 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 34 transitions.
[2025-04-28 21:21:28,806 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 34 transitions. Word has length 30
[2025-04-28 21:21:28,807 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,807 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 34 transitions.
[2025-04-28 21:21:28,807 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:28,807 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 34 transitions.
[2025-04-28 21:21:28,808 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:28,808 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,808 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 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:28,816 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:29,014 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:29,015 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,015 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,016 INFO  L85        PathProgramCache]: Analyzing trace with hash 940466396, now seen corresponding path program 1 times
[2025-04-28 21:21:29,016 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,016 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1675905471]
[2025-04-28 21:21:29,016 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,016 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,026 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:29,052 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:29,055 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,056 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,179 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:29,179 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,180 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1675905471]
[2025-04-28 21:21:29,180 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1675905471] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,180 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1284334785]
[2025-04-28 21:21:29,180 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,180 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,183 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,185 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:29,189 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,253 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:29,285 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:29,285 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,285 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,286 INFO  L256         TraceCheckSpWp]: Trace formula consists of 115 conjuncts, 3 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,288 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,306 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:29,306 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:29,306 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1284334785] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,306 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:29,307 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 4
[2025-04-28 21:21:29,307 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1041113019]
[2025-04-28 21:21:29,307 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,307 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:29,308 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,309 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:29,310 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:29,310 INFO  L87              Difference]: Start difference. First operand 29 states and 34 transitions. Second operand  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:29,337 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,339 INFO  L93              Difference]: Finished difference Result 29 states and 33 transitions.
[2025-04-28 21:21:29,340 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:29,340 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8) Word has length 30
[2025-04-28 21:21:29,341 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,341 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:21:29,341 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:29,342 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 31 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:29,342 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 1 mSDsluCounter, 46 mSDsCounter, 0 mSdLazyCounter, 5 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 75 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 5 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,345 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 75 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 5 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:29,346 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:29,351 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:29,353 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 8 states have call successors, (8), 6 states have call predecessors, (8), 7 states have return successors, (10), 8 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:29,354 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 30 transitions.
[2025-04-28 21:21:29,355 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 30 transitions. Word has length 30
[2025-04-28 21:21:29,355 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,355 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 30 transitions.
[2025-04-28 21:21:29,356 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.333333333333333) internal successors, (13), 4 states have internal predecessors, (13), 3 states have call successors, (8), 2 states have call predecessors, (8), 3 states have return successors, (8), 2 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:29,356 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 30 transitions.
[2025-04-28 21:21:29,357 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 31
[2025-04-28 21:21:29,358 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,358 INFO  L218           NwaCegarLoop]: trace histogram [3, 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, 1]
[2025-04-28 21:21:29,363 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:29,559 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:29,559 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,559 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,560 INFO  L85        PathProgramCache]: Analyzing trace with hash -893693228, now seen corresponding path program 1 times
[2025-04-28 21:21:29,560 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,560 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [640314925]
[2025-04-28 21:21:29,560 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,560 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,570 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:29,589 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:29,592 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,592 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,923 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:29,924 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,924 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [640314925]
[2025-04-28 21:21:29,924 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [640314925] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,924 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [38636322]
[2025-04-28 21:21:29,924 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,924 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,927 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,929 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:29,932 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,973 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 30 statements into 1 equivalence classes.
[2025-04-28 21:21:29,996 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 30 of 30 statements.
[2025-04-28 21:21:29,996 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,996 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,997 INFO  L256         TraceCheckSpWp]: Trace formula consists of 115 conjuncts, 16 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:30,000 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:30,371 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:30,373 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:32,970 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:32,971 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [38636322] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:32,971 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:32,971 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 12
[2025-04-28 21:21:32,971 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1065861979]
[2025-04-28 21:21:32,971 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,973 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:32,974 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,975 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:32,975 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=103, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:32,975 INFO  L87              Difference]: Start difference. First operand 27 states and 30 transitions. Second operand  has 12 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 12 states have internal predecessors, (19), 8 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 7 states have call predecessors, (14), 8 states have call successors, (14)
[2025-04-28 21:21:33,122 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,123 INFO  L93              Difference]: Finished difference Result 36 states and 44 transitions.
[2025-04-28 21:21:33,124 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:33,124 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 12 states have internal predecessors, (19), 8 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 7 states have call predecessors, (14), 8 states have call successors, (14) Word has length 30
[2025-04-28 21:21:33,125 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,126 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:33,127 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:33,127 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 67 GetRequests, 54 SyntacticMatches, 2 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:33,130 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 6 mSDsluCounter, 149 mSDsCounter, 0 mSdLazyCounter, 80 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 171 SdHoareTripleChecker+Invalid, 83 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 80 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,132 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 171 Invalid, 83 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 80 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:33,133 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:33,140 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 34.
[2025-04-28 21:21:33,142 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 14 states have (on average 1.0714285714285714) internal successors, (15), 14 states have internal predecessors, (15), 10 states have call successors, (10), 7 states have call predecessors, (10), 9 states have return successors, (17), 12 states have call predecessors, (17), 10 states have call successors, (17)
[2025-04-28 21:21:33,143 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 42 transitions.
[2025-04-28 21:21:33,143 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 42 transitions. Word has length 30
[2025-04-28 21:21:33,144 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,144 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 42 transitions.
[2025-04-28 21:21:33,144 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 12 states have internal predecessors, (19), 8 states have call successors, (14), 1 states have call predecessors, (14), 6 states have return successors, (14), 7 states have call predecessors, (14), 8 states have call successors, (14)
[2025-04-28 21:21:33,144 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 42 transitions.
[2025-04-28 21:21:33,149 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 61
[2025-04-28 21:21:33,149 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,149 INFO  L218           NwaCegarLoop]: trace histogram [7, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,156 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:33,350 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:33,350 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,350 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,351 INFO  L85        PathProgramCache]: Analyzing trace with hash -110529360, now seen corresponding path program 2 times
[2025-04-28 21:21:33,351 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,351 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2042318802]
[2025-04-28 21:21:33,351 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:33,351 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,375 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:33,404 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:33,407 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:33,407 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,925 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 14 proven. 33 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:33,927 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,927 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2042318802]
[2025-04-28 21:21:33,927 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2042318802] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,927 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1480006297]
[2025-04-28 21:21:33,927 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:33,927 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,930 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,932 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:33,948 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,010 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 60 statements into 2 equivalence classes.
[2025-04-28 21:21:34,050 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 60 of 60 statements.
[2025-04-28 21:21:34,051 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:34,051 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,052 INFO  L256         TraceCheckSpWp]: Trace formula consists of 253 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,055 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,348 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 33 proven. 20 refuted. 0 times theorem prover too weak. 37 trivial. 0 not checked.
[2025-04-28 21:21:34,352 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:39,644 INFO  L134       CoverageAnalysis]: Checked inductivity of 90 backedges. 34 proven. 20 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:39,644 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1480006297] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:39,644 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:39,644 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 12, 13] total 21
[2025-04-28 21:21:39,644 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [953175224]
[2025-04-28 21:21:39,645 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,645 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:39,645 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,646 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:39,646 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=66, Invalid=354, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:39,647 INFO  L87              Difference]: Start difference. First operand 34 states and 42 transitions. Second operand  has 21 states, 11 states have (on average 2.6363636363636362) internal successors, (29), 19 states have internal predecessors, (29), 15 states have call successors, (26), 1 states have call predecessors, (26), 11 states have return successors, (31), 16 states have call predecessors, (31), 15 states have call successors, (31)
[2025-04-28 21:21:40,108 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,108 INFO  L93              Difference]: Finished difference Result 61 states and 92 transitions.
[2025-04-28 21:21:40,108 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:21:40,109 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 11 states have (on average 2.6363636363636362) internal successors, (29), 19 states have internal predecessors, (29), 15 states have call successors, (26), 1 states have call predecessors, (26), 11 states have return successors, (31), 16 states have call predecessors, (31), 15 states have call successors, (31) Word has length 60
[2025-04-28 21:21:40,109 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,110 INFO  L225             Difference]: With dead ends: 61
[2025-04-28 21:21:40,110 INFO  L226             Difference]: Without dead ends: 61
[2025-04-28 21:21:40,111 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 138 GetRequests, 107 SyntacticMatches, 4 SemanticMatches, 27 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 156 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=145, Invalid=667, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:21:40,112 INFO  L437           NwaCegarLoop]: 33 mSDtfsCounter, 19 mSDsluCounter, 285 mSDsCounter, 0 mSdLazyCounter, 168 mSolverCounterSat, 68 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 318 SdHoareTripleChecker+Invalid, 236 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 68 IncrementalHoareTripleChecker+Valid, 168 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,112 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 318 Invalid, 236 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [68 Valid, 168 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:40,113 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 61 states.
[2025-04-28 21:21:40,121 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 61 to 58.
[2025-04-28 21:21:40,121 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 58 states, 23 states have (on average 1.0869565217391304) internal successors, (25), 24 states have internal predecessors, (25), 18 states have call successors, (18), 9 states have call predecessors, (18), 16 states have return successors, (44), 24 states have call predecessors, (44), 18 states have call successors, (44)
[2025-04-28 21:21:40,123 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 87 transitions.
[2025-04-28 21:21:40,123 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 87 transitions. Word has length 60
[2025-04-28 21:21:40,123 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,123 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 87 transitions.
[2025-04-28 21:21:40,123 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 11 states have (on average 2.6363636363636362) internal successors, (29), 19 states have internal predecessors, (29), 15 states have call successors, (26), 1 states have call predecessors, (26), 11 states have return successors, (31), 16 states have call predecessors, (31), 15 states have call successors, (31)
[2025-04-28 21:21:40,124 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 87 transitions.
[2025-04-28 21:21:40,128 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 151
[2025-04-28 21:21:40,128 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,128 INFO  L218           NwaCegarLoop]: trace histogram [19, 10, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,136 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:40,332 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:40,333 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,333 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,333 INFO  L85        PathProgramCache]: Analyzing trace with hash 365538700, now seen corresponding path program 3 times
[2025-04-28 21:21:40,333 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,333 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [796183789]
[2025-04-28 21:21:40,333 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:40,334 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,354 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 150 statements into 11 equivalence classes.
[2025-04-28 21:21:40,416 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s) and asserted 79 of 150 statements.
[2025-04-28 21:21:40,416 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s)
[2025-04-28 21:21:40,416 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,568 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 210 proven. 35 refuted. 0 times theorem prover too weak. 592 trivial. 0 not checked.
[2025-04-28 21:21:41,569 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,569 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [796183789]
[2025-04-28 21:21:41,569 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [796183789] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,569 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [806334279]
[2025-04-28 21:21:41,569 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:41,569 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,572 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,574 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:41,578 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,689 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 150 statements into 11 equivalence classes.
[2025-04-28 21:21:41,746 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s) and asserted 79 of 150 statements.
[2025-04-28 21:21:41,747 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s)
[2025-04-28 21:21:41,747 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,749 INFO  L256         TraceCheckSpWp]: Trace formula consists of 367 conjuncts, 33 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,754 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,362 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 221 proven. 62 refuted. 0 times theorem prover too weak. 554 trivial. 0 not checked.
[2025-04-28 21:21:42,364 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,115 INFO  L134       CoverageAnalysis]: Checked inductivity of 837 backedges. 225 proven. 61 refuted. 0 times theorem prover too weak. 551 trivial. 0 not checked.
[2025-04-28 21:21:52,115 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [806334279] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,115 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,115 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 15, 17] total 32
[2025-04-28 21:21:52,115 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2027517744]
[2025-04-28 21:21:52,115 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,116 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 32 states
[2025-04-28 21:21:52,116 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,117 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 32 interpolants.
[2025-04-28 21:21:52,118 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=138, Invalid=854, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:52,119 INFO  L87              Difference]: Start difference. First operand 58 states and 87 transitions. Second operand  has 32 states, 17 states have (on average 2.3529411764705883) internal successors, (40), 30 states have internal predecessors, (40), 24 states have call successors, (38), 1 states have call predecessors, (38), 17 states have return successors, (44), 26 states have call predecessors, (44), 24 states have call successors, (44)
[2025-04-28 21:21:52,786 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,786 INFO  L93              Difference]: Finished difference Result 99 states and 174 transitions.
[2025-04-28 21:21:52,789 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:21:52,790 INFO  L79                 Accepts]: Start accepts. Automaton has  has 32 states, 17 states have (on average 2.3529411764705883) internal successors, (40), 30 states have internal predecessors, (40), 24 states have call successors, (38), 1 states have call predecessors, (38), 17 states have return successors, (44), 26 states have call predecessors, (44), 24 states have call successors, (44) Word has length 150
[2025-04-28 21:21:52,791 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,792 INFO  L225             Difference]: With dead ends: 99
[2025-04-28 21:21:52,792 INFO  L226             Difference]: Without dead ends: 99
[2025-04-28 21:21:52,795 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 321 GetRequests, 280 SyntacticMatches, 3 SemanticMatches, 38 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 428 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=253, Invalid=1307, Unknown=0, NotChecked=0, Total=1560
[2025-04-28 21:21:52,796 INFO  L437           NwaCegarLoop]: 29 mSDtfsCounter, 40 mSDsluCounter, 329 mSDsCounter, 0 mSdLazyCounter, 192 mSolverCounterSat, 196 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 41 SdHoareTripleChecker+Valid, 358 SdHoareTripleChecker+Invalid, 388 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 196 IncrementalHoareTripleChecker+Valid, 192 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,796 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [41 Valid, 358 Invalid, 388 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [196 Valid, 192 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:52,797 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 99 states.
[2025-04-28 21:21:52,825 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 99 to 76.
[2025-04-28 21:21:52,826 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 76 states, 30 states have (on average 1.0666666666666667) internal successors, (32), 30 states have internal predecessors, (32), 25 states have call successors, (25), 12 states have call predecessors, (25), 20 states have return successors, (65), 33 states have call predecessors, (65), 25 states have call successors, (65)
[2025-04-28 21:21:52,830 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 76 states to 76 states and 122 transitions.
[2025-04-28 21:21:52,830 INFO  L79                 Accepts]: Start accepts. Automaton has 76 states and 122 transitions. Word has length 150
[2025-04-28 21:21:52,830 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,830 INFO  L485      AbstractCegarLoop]: Abstraction has 76 states and 122 transitions.
[2025-04-28 21:21:52,831 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 32 states, 17 states have (on average 2.3529411764705883) internal successors, (40), 30 states have internal predecessors, (40), 24 states have call successors, (38), 1 states have call predecessors, (38), 17 states have return successors, (44), 26 states have call predecessors, (44), 24 states have call successors, (44)
[2025-04-28 21:21:52,831 INFO  L278                IsEmpty]: Start isEmpty. Operand 76 states and 122 transitions.
[2025-04-28 21:21:52,845 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 451
[2025-04-28 21:21:52,847 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,847 INFO  L218           NwaCegarLoop]: trace histogram [59, 30, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,853 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:53,051 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:53,052 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,052 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,052 INFO  L85        PathProgramCache]: Analyzing trace with hash -1796965356, now seen corresponding path program 4 times
[2025-04-28 21:21:53,052 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,052 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [251960124]
[2025-04-28 21:21:53,052 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:53,052 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,106 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 450 statements into 2 equivalence classes.
[2025-04-28 21:21:53,230 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 449 of 450 statements.
[2025-04-28 21:21:53,231 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:53,231 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,148 INFO  L134       CoverageAnalysis]: Checked inductivity of 8787 backedges. 845 proven. 1410 refuted. 0 times theorem prover too weak. 6532 trivial. 0 not checked.
[2025-04-28 21:21:57,149 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,149 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [251960124]
[2025-04-28 21:21:57,149 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [251960124] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,150 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [215843233]
[2025-04-28 21:21:57,150 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:57,151 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,153 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,155 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:57,158 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,474 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 450 statements into 2 equivalence classes.
[2025-04-28 21:21:57,788 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 449 of 450 statements.
[2025-04-28 21:21:57,788 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:57,788 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,797 INFO  L256         TraceCheckSpWp]: Trace formula consists of 2033 conjuncts, 45 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,806 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,385 INFO  L134       CoverageAnalysis]: Checked inductivity of 8787 backedges. 1686 proven. 625 refuted. 0 times theorem prover too weak. 6476 trivial. 0 not checked.
[2025-04-28 21:21:58,385 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
