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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:18,185 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:18,261 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f546a589-7b22-4df4-87d3-b41a2da7d9e5/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:18,266 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:18,267 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:18,294 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:18,295 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:18,295 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:18,295 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:18,295 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:18,296 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:18,296 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:18,296 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:18,296 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:18,297 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:18,297 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:18,297 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:18,297 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:18,297 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:18,297 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:18,298 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:18,298 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:18,298 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:18,298 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:18,298 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:18,299 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:18,299 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:18,721 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:18,733 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:18,736 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:18,739 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:18,740 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:18,741 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f546a589-7b22-4df4-87d3-b41a2da7d9e5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-105.smt2
[2025-04-28 21:21:18,744 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:18,748 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:19,008 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f546a589-7b22-4df4-87d3-b41a2da7d9e5/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-105.smt2
[2025-04-28 21:21:19,016 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:19,020 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:19,021 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:19,021 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:19,021 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:19,025 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,068 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19 Unit
[2025-04-28 21:21:19,069 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:19,071 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:19,071 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:19,071 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:19,094 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,094 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,126 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,127 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,130 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,130 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,133 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,134 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,135 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,150 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:19,151 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:19,152 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:19,152 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:19,153 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,156 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:19,173 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:19,190 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:19,194 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:19,214 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:19,214 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:19,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:19,215 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv5 given in one single declaration
[2025-04-28 21:21:19,215 INFO  L130     BoogieDeclarations]: Found specification of procedure inv5
[2025-04-28 21:21:19,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv5
[2025-04-28 21:21:19,215 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv4 given in one single declaration
[2025-04-28 21:21:19,215 INFO  L130     BoogieDeclarations]: Found specification of procedure inv4
[2025-04-28 21:21:19,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv4
[2025-04-28 21:21:19,215 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv3 given in one single declaration
[2025-04-28 21:21:19,215 INFO  L130     BoogieDeclarations]: Found specification of procedure inv3
[2025-04-28 21:21:19,215 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv3
[2025-04-28 21:21:19,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv2 given in one single declaration
[2025-04-28 21:21:19,216 INFO  L130     BoogieDeclarations]: Found specification of procedure inv2
[2025-04-28 21:21:19,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv2
[2025-04-28 21:21:19,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:19,216 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:19,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:19,216 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:19,216 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:19,216 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:19,301 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:19,305 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:19,486 INFO  L?                        ?]: Removed 3 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:19,490 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:19,512 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:19,513 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:19,513 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:19 BoogieIcfgContainer
[2025-04-28 21:21:19,513 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:19,517 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:19,521 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:19,526 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:19,526 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/3) ...
[2025-04-28 21:21:19,528 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1b71c485 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:19, skipping insertion in model container
[2025-04-28 21:21:19,528 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (2/3) ...
[2025-04-28 21:21:19,529 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1b71c485 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:19, skipping insertion in model container
[2025-04-28 21:21:19,529 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:19" (3/3) ...
[2025-04-28 21:21:19,531 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:19,553 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:19,557 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 7 procedures, 33 locations, 53 edges, 7 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:19,626 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:19,652 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;@76760701, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:19,652 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:19,657 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 33 states, 14 states have (on average 1.4285714285714286) internal successors, (20), 20 states have internal predecessors, (20), 11 states have call successors, (11), 6 states have call predecessors, (11), 6 states have return successors, (11), 7 states have call predecessors, (11), 11 states have call successors, (11)
[2025-04-28 21:21:19,670 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:19,671 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,672 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,673 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,681 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,682 INFO  L85        PathProgramCache]: Analyzing trace with hash 99699606, now seen corresponding path program 1 times
[2025-04-28 21:21:19,692 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,692 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [259876326]
[2025-04-28 21:21:19,692 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,693 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,739 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:19,767 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:19,767 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,768 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,177 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:20,181 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,182 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [259876326]
[2025-04-28 21:21:20,183 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [259876326] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,187 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,190 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:20,192 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1455708594]
[2025-04-28 21:21:20,195 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,202 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:20,204 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,245 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:20,246 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:20,251 INFO  L87              Difference]: Start difference. First operand  has 33 states, 14 states have (on average 1.4285714285714286) internal successors, (20), 20 states have internal predecessors, (20), 11 states have call successors, (11), 6 states have call predecessors, (11), 6 states have return successors, (11), 7 states have call predecessors, (11), 11 states have call successors, (11) Second operand  has 8 states, 7 states have (on average 1.8571428571428572) internal successors, (13), 8 states have internal predecessors, (13), 2 states have call successors, (6), 1 states have call predecessors, (6), 6 states have return successors, (6), 5 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:20,488 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,489 INFO  L93              Difference]: Finished difference Result 41 states and 54 transitions.
[2025-04-28 21:21:20,499 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:20,500 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 7 states have (on average 1.8571428571428572) internal successors, (13), 8 states have internal predecessors, (13), 2 states have call successors, (6), 1 states have call predecessors, (6), 6 states have return successors, (6), 5 states have call predecessors, (6), 2 states have call successors, (6) Word has length 25
[2025-04-28 21:21:20,501 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,509 INFO  L225             Difference]: With dead ends: 41
[2025-04-28 21:21:20,510 INFO  L226             Difference]: Without dead ends: 41
[2025-04-28 21:21:20,513 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:20,521 INFO  L437           NwaCegarLoop]: 31 mSDtfsCounter, 1 mSDsluCounter, 167 mSDsCounter, 0 mSdLazyCounter, 78 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 198 SdHoareTripleChecker+Invalid, 78 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 78 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,522 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 198 Invalid, 78 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 78 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:20,541 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 41 states.
[2025-04-28 21:21:20,612 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 41 to 41.
[2025-04-28 21:21:20,617 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 18 states have (on average 1.2777777777777777) internal successors, (23), 23 states have internal predecessors, (23), 11 states have call successors, (11), 6 states have call predecessors, (11), 11 states have return successors, (20), 11 states have call predecessors, (20), 11 states have call successors, (20)
[2025-04-28 21:21:20,625 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 54 transitions.
[2025-04-28 21:21:20,627 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 54 transitions. Word has length 25
[2025-04-28 21:21:20,628 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,628 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 54 transitions.
[2025-04-28 21:21:20,628 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 7 states have (on average 1.8571428571428572) internal successors, (13), 8 states have internal predecessors, (13), 2 states have call successors, (6), 1 states have call predecessors, (6), 6 states have return successors, (6), 5 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:20,628 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 54 transitions.
[2025-04-28 21:21:20,631 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:20,631 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,631 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,632 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:20,632 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,633 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,633 INFO  L85        PathProgramCache]: Analyzing trace with hash -1960406885, now seen corresponding path program 1 times
[2025-04-28 21:21:20,633 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,633 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [299312381]
[2025-04-28 21:21:20,633 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,634 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,643 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:20,679 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:20,680 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,680 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,287 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:21,288 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,289 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [299312381]
[2025-04-28 21:21:21,289 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [299312381] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:21,289 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1490462215]
[2025-04-28 21:21:21,289 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,289 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:21,295 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:21,300 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:21,302 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:21,374 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:21,418 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:21,418 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,418 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,421 INFO  L256         TraceCheckSpWp]: Trace formula consists of 100 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:21,434 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:21,867 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:21,868 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:24,544 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:24,544 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1490462215] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:24,544 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:24,545 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 9] total 18
[2025-04-28 21:21:24,545 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1534825020]
[2025-04-28 21:21:24,546 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:24,546 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:24,549 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:24,551 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:24,552 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=43, Invalid=263, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:24,552 INFO  L87              Difference]: Start difference. First operand 41 states and 54 transitions. Second operand  has 18 states, 13 states have (on average 2.0) internal successors, (26), 18 states have internal predecessors, (26), 7 states have call successors, (11), 1 states have call predecessors, (11), 13 states have return successors, (15), 11 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:21:24,931 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:24,931 INFO  L93              Difference]: Finished difference Result 55 states and 72 transitions.
[2025-04-28 21:21:24,933 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:24,933 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 13 states have (on average 2.0) internal successors, (26), 18 states have internal predecessors, (26), 7 states have call successors, (11), 1 states have call predecessors, (11), 13 states have return successors, (15), 11 states have call predecessors, (15), 7 states have call successors, (15) Word has length 29
[2025-04-28 21:21:24,933 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:24,935 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:24,935 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:24,936 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 71 GetRequests, 50 SyntacticMatches, 1 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 47 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=69, Invalid=393, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:24,937 INFO  L437           NwaCegarLoop]: 39 mSDtfsCounter, 4 mSDsluCounter, 364 mSDsCounter, 0 mSdLazyCounter, 187 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 403 SdHoareTripleChecker+Invalid, 196 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 187 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:24,937 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 403 Invalid, 196 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 187 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:24,940 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:24,954 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 47.
[2025-04-28 21:21:24,954 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 47 states, 21 states have (on average 1.2857142857142858) internal successors, (27), 26 states have internal predecessors, (27), 12 states have call successors, (12), 7 states have call predecessors, (12), 13 states have return successors, (23), 13 states have call predecessors, (23), 12 states have call successors, (23)
[2025-04-28 21:21:24,956 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 47 states to 47 states and 62 transitions.
[2025-04-28 21:21:24,958 INFO  L79                 Accepts]: Start accepts. Automaton has 47 states and 62 transitions. Word has length 29
[2025-04-28 21:21:24,958 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:24,958 INFO  L485      AbstractCegarLoop]: Abstraction has 47 states and 62 transitions.
[2025-04-28 21:21:24,959 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 13 states have (on average 2.0) internal successors, (26), 18 states have internal predecessors, (26), 7 states have call successors, (11), 1 states have call predecessors, (11), 13 states have return successors, (15), 11 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:21:24,959 INFO  L278                IsEmpty]: Start isEmpty. Operand 47 states and 62 transitions.
[2025-04-28 21:21:24,961 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:24,962 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,962 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:24,969 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:25,167 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,167 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,168 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,168 INFO  L85        PathProgramCache]: Analyzing trace with hash 1387288923, now seen corresponding path program 1 times
[2025-04-28 21:21:25,168 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,168 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1522490205]
[2025-04-28 21:21:25,168 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,169 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,175 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:25,191 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:25,193 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,193 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,451 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:25,451 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,451 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1522490205]
[2025-04-28 21:21:25,451 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1522490205] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:25,451 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1935092111]
[2025-04-28 21:21:25,451 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,451 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,457 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:25,459 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:25,465 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:25,532 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:25,553 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:25,554 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,554 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,559 INFO  L256         TraceCheckSpWp]: Trace formula consists of 100 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:25,561 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:25,840 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:25,840 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:27,830 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:27,830 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1935092111] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:27,831 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:27,831 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 9] total 18
[2025-04-28 21:21:27,831 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1591379995]
[2025-04-28 21:21:27,831 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,832 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:27,832 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,832 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:27,833 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=264, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:27,833 INFO  L87              Difference]: Start difference. First operand 47 states and 62 transitions. Second operand  has 18 states, 13 states have (on average 2.0) internal successors, (26), 18 states have internal predecessors, (26), 7 states have call successors, (11), 1 states have call predecessors, (11), 13 states have return successors, (15), 11 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:21:28,127 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,127 INFO  L93              Difference]: Finished difference Result 63 states and 82 transitions.
[2025-04-28 21:21:28,128 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:21:28,129 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 13 states have (on average 2.0) internal successors, (26), 18 states have internal predecessors, (26), 7 states have call successors, (11), 1 states have call predecessors, (11), 13 states have return successors, (15), 11 states have call predecessors, (15), 7 states have call successors, (15) Word has length 29
[2025-04-28 21:21:28,129 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,131 INFO  L225             Difference]: With dead ends: 63
[2025-04-28 21:21:28,132 INFO  L226             Difference]: Without dead ends: 63
[2025-04-28 21:21:28,132 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 71 GetRequests, 49 SyntacticMatches, 2 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 45 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=67, Invalid=395, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:28,133 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 4 mSDsluCounter, 372 mSDsCounter, 0 mSdLazyCounter, 207 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 412 SdHoareTripleChecker+Invalid, 217 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 207 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,134 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 412 Invalid, 217 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 207 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:28,135 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 63 states.
[2025-04-28 21:21:28,144 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 63 to 53.
[2025-04-28 21:21:28,144 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 53 states, 24 states have (on average 1.2916666666666667) internal successors, (31), 29 states have internal predecessors, (31), 13 states have call successors, (13), 8 states have call predecessors, (13), 15 states have return successors, (27), 15 states have call predecessors, (27), 13 states have call successors, (27)
[2025-04-28 21:21:28,146 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 53 states to 53 states and 71 transitions.
[2025-04-28 21:21:28,146 INFO  L79                 Accepts]: Start accepts. Automaton has 53 states and 71 transitions. Word has length 29
[2025-04-28 21:21:28,146 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,146 INFO  L485      AbstractCegarLoop]: Abstraction has 53 states and 71 transitions.
[2025-04-28 21:21:28,146 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 13 states have (on average 2.0) internal successors, (26), 18 states have internal predecessors, (26), 7 states have call successors, (11), 1 states have call predecessors, (11), 13 states have return successors, (15), 11 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:21:28,146 INFO  L278                IsEmpty]: Start isEmpty. Operand 53 states and 71 transitions.
[2025-04-28 21:21:28,148 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:28,148 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,148 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,152 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:28,348 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,349 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,349 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,349 INFO  L85        PathProgramCache]: Analyzing trace with hash -487757829, now seen corresponding path program 1 times
[2025-04-28 21:21:28,349 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,349 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [400972553]
[2025-04-28 21:21:28,350 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,350 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,355 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:28,368 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:28,368 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,368 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,591 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:28,591 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,591 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [400972553]
[2025-04-28 21:21:28,592 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [400972553] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,592 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,592 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [] total 9
[2025-04-28 21:21:28,592 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1609598086]
[2025-04-28 21:21:28,592 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,592 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:28,593 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,593 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:28,593 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=15, Invalid=57, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:28,594 INFO  L87              Difference]: Start difference. First operand 53 states and 71 transitions. Second operand  has 9 states, 7 states have (on average 2.142857142857143) internal successors, (15), 9 states have internal predecessors, (15), 3 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:28,753 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,753 INFO  L93              Difference]: Finished difference Result 65 states and 84 transitions.
[2025-04-28 21:21:28,754 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:28,754 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 7 states have (on average 2.142857142857143) internal successors, (15), 9 states have internal predecessors, (15), 3 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7) Word has length 29
[2025-04-28 21:21:28,755 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,756 INFO  L225             Difference]: With dead ends: 65
[2025-04-28 21:21:28,756 INFO  L226             Difference]: Without dead ends: 63
[2025-04-28 21:21:28,756 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=19, Invalid=71, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:28,757 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 3 mSDsluCounter, 213 mSDsCounter, 0 mSdLazyCounter, 107 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 248 SdHoareTripleChecker+Invalid, 107 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 107 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,757 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 248 Invalid, 107 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 107 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:28,758 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 63 states.
[2025-04-28 21:21:28,768 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 63 to 57.
[2025-04-28 21:21:28,768 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 26 states have (on average 1.2692307692307692) internal successors, (33), 31 states have internal predecessors, (33), 13 states have call successors, (13), 8 states have call predecessors, (13), 17 states have return successors, (29), 17 states have call predecessors, (29), 13 states have call successors, (29)
[2025-04-28 21:21:28,769 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 75 transitions.
[2025-04-28 21:21:28,770 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 75 transitions. Word has length 29
[2025-04-28 21:21:28,770 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,772 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 75 transitions.
[2025-04-28 21:21:28,772 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 7 states have (on average 2.142857142857143) internal successors, (15), 9 states have internal predecessors, (15), 3 states have call successors, (7), 1 states have call predecessors, (7), 6 states have return successors, (7), 5 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:28,773 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 75 transitions.
[2025-04-28 21:21:28,774 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:28,774 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,774 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,774 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:28,774 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,775 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,775 INFO  L85        PathProgramCache]: Analyzing trace with hash -1690891141, now seen corresponding path program 1 times
[2025-04-28 21:21:28,775 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,775 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [18171925]
[2025-04-28 21:21:28,775 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,775 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,784 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:28,789 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:28,790 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,790 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,972 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:28,973 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,973 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [18171925]
[2025-04-28 21:21:28,973 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [18171925] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,973 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [384503377]
[2025-04-28 21:21:28,973 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,973 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,977 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,979 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:28,982 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,060 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:29,090 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:29,090 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,090 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,092 INFO  L256         TraceCheckSpWp]: Trace formula consists of 100 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,094 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,283 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:29,284 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:30,920 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:30,921 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [384503377] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:30,921 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:30,921 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 9] total 18
[2025-04-28 21:21:30,921 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [703986073]
[2025-04-28 21:21:30,922 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,924 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:30,924 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,925 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:30,926 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=41, Invalid=265, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:30,927 INFO  L87              Difference]: Start difference. First operand 57 states and 75 transitions. Second operand  has 18 states, 13 states have (on average 2.0) internal successors, (26), 18 states have internal predecessors, (26), 7 states have call successors, (11), 1 states have call predecessors, (11), 13 states have return successors, (15), 11 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:21:31,279 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,279 INFO  L93              Difference]: Finished difference Result 71 states and 92 transitions.
[2025-04-28 21:21:31,279 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:21:31,280 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 13 states have (on average 2.0) internal successors, (26), 18 states have internal predecessors, (26), 7 states have call successors, (11), 1 states have call predecessors, (11), 13 states have return successors, (15), 11 states have call predecessors, (15), 7 states have call successors, (15) Word has length 29
[2025-04-28 21:21:31,280 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,281 INFO  L225             Difference]: With dead ends: 71
[2025-04-28 21:21:31,281 INFO  L226             Difference]: Without dead ends: 69
[2025-04-28 21:21:31,282 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 72 GetRequests, 48 SyntacticMatches, 3 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 47 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=70, Invalid=436, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:31,283 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 4 mSDsluCounter, 393 mSDsCounter, 0 mSdLazyCounter, 225 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 429 SdHoareTripleChecker+Invalid, 237 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 225 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,283 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 429 Invalid, 237 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 225 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:31,284 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 69 states.
[2025-04-28 21:21:31,294 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 69 to 61.
[2025-04-28 21:21:31,295 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 61 states, 28 states have (on average 1.2857142857142858) internal successors, (36), 33 states have internal predecessors, (36), 14 states have call successors, (14), 9 states have call predecessors, (14), 18 states have return successors, (32), 18 states have call predecessors, (32), 14 states have call successors, (32)
[2025-04-28 21:21:31,296 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 61 states to 61 states and 82 transitions.
[2025-04-28 21:21:31,297 INFO  L79                 Accepts]: Start accepts. Automaton has 61 states and 82 transitions. Word has length 29
[2025-04-28 21:21:31,297 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,297 INFO  L485      AbstractCegarLoop]: Abstraction has 61 states and 82 transitions.
[2025-04-28 21:21:31,297 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 13 states have (on average 2.0) internal successors, (26), 18 states have internal predecessors, (26), 7 states have call successors, (11), 1 states have call predecessors, (11), 13 states have return successors, (15), 11 states have call predecessors, (15), 7 states have call successors, (15)
[2025-04-28 21:21:31,297 INFO  L278                IsEmpty]: Start isEmpty. Operand 61 states and 82 transitions.
[2025-04-28 21:21:31,299 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:31,299 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,299 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,304 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:31,503 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:31,503 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,503 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,504 INFO  L85        PathProgramCache]: Analyzing trace with hash 1633087994, now seen corresponding path program 1 times
[2025-04-28 21:21:31,504 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,504 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [980472555]
[2025-04-28 21:21:31,504 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,504 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,513 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:31,520 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:31,520 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,520 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,698 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:31,698 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,698 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [980472555]
[2025-04-28 21:21:31,698 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [980472555] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,698 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2085972651]
[2025-04-28 21:21:31,698 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,699 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,702 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,704 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:31,708 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,791 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:31,807 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:31,807 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,807 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,808 INFO  L256         TraceCheckSpWp]: Trace formula consists of 100 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,821 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,011 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:32,011 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:32,012 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2085972651] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,012 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:32,012 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [10] imperfect sequences [10] total 17
[2025-04-28 21:21:32,013 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2037710548]
[2025-04-28 21:21:32,013 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,013 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:32,013 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,014 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:32,014 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=234, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:32,014 INFO  L87              Difference]: Start difference. First operand 61 states and 82 transitions. Second operand  has 10 states, 8 states have (on average 1.875) internal successors, (15), 10 states have internal predecessors, (15), 3 states have call successors, (7), 1 states have call predecessors, (7), 7 states have return successors, (7), 6 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:32,133 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,133 INFO  L93              Difference]: Finished difference Result 67 states and 88 transitions.
[2025-04-28 21:21:32,134 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:32,134 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 1.875) internal successors, (15), 10 states have internal predecessors, (15), 3 states have call successors, (7), 1 states have call predecessors, (7), 7 states have return successors, (7), 6 states have call predecessors, (7), 3 states have call successors, (7) Word has length 29
[2025-04-28 21:21:32,134 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,135 INFO  L225             Difference]: With dead ends: 67
[2025-04-28 21:21:32,135 INFO  L226             Difference]: Without dead ends: 67
[2025-04-28 21:21:32,136 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=38, Invalid=234, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:32,136 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 1 mSDsluCounter, 264 mSDsCounter, 0 mSdLazyCounter, 103 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 302 SdHoareTripleChecker+Invalid, 104 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 103 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,137 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 302 Invalid, 104 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 103 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:32,138 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 67 states.
[2025-04-28 21:21:32,147 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 67 to 57.
[2025-04-28 21:21:32,147 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 26 states have (on average 1.3076923076923077) internal successors, (34), 31 states have internal predecessors, (34), 14 states have call successors, (14), 9 states have call predecessors, (14), 16 states have return successors, (29), 16 states have call predecessors, (29), 14 states have call successors, (29)
[2025-04-28 21:21:32,148 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 77 transitions.
[2025-04-28 21:21:32,149 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 77 transitions. Word has length 29
[2025-04-28 21:21:32,149 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,149 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 77 transitions.
[2025-04-28 21:21:32,149 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 1.875) internal successors, (15), 10 states have internal predecessors, (15), 3 states have call successors, (7), 1 states have call predecessors, (7), 7 states have return successors, (7), 6 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:32,149 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 77 transitions.
[2025-04-28 21:21:32,151 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:32,151 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,151 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,157 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:32,355 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:32,355 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,356 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,356 INFO  L85        PathProgramCache]: Analyzing trace with hash -1324828032, now seen corresponding path program 1 times
[2025-04-28 21:21:32,356 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,356 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1714811705]
[2025-04-28 21:21:32,356 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,356 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,361 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:32,370 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:32,370 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,370 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,576 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:32,576 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,576 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1714811705]
[2025-04-28 21:21:32,576 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1714811705] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,576 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:32,576 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:32,576 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1909009765]
[2025-04-28 21:21:32,576 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,577 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:32,577 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,578 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:32,578 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=90, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:32,578 INFO  L87              Difference]: Start difference. First operand 57 states and 77 transitions. Second operand  has 11 states, 8 states have (on average 2.125) internal successors, (17), 11 states have internal predecessors, (17), 4 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (8), 6 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:32,810 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,810 INFO  L93              Difference]: Finished difference Result 69 states and 90 transitions.
[2025-04-28 21:21:32,810 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:32,811 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 8 states have (on average 2.125) internal successors, (17), 11 states have internal predecessors, (17), 4 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (8), 6 states have call predecessors, (8), 4 states have call successors, (8) Word has length 33
[2025-04-28 21:21:32,811 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,812 INFO  L225             Difference]: With dead ends: 69
[2025-04-28 21:21:32,812 INFO  L226             Difference]: Without dead ends: 65
[2025-04-28 21:21:32,812 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=29, Invalid=127, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:32,813 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 4 mSDsluCounter, 269 mSDsCounter, 0 mSdLazyCounter, 160 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 309 SdHoareTripleChecker+Invalid, 160 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 160 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,813 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 309 Invalid, 160 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 160 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:32,814 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 65 states.
[2025-04-28 21:21:32,823 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 65 to 61.
[2025-04-28 21:21:32,823 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 61 states, 28 states have (on average 1.2857142857142858) internal successors, (36), 33 states have internal predecessors, (36), 14 states have call successors, (14), 9 states have call predecessors, (14), 18 states have return successors, (32), 18 states have call predecessors, (32), 14 states have call successors, (32)
[2025-04-28 21:21:32,825 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 61 states to 61 states and 82 transitions.
[2025-04-28 21:21:32,825 INFO  L79                 Accepts]: Start accepts. Automaton has 61 states and 82 transitions. Word has length 33
[2025-04-28 21:21:32,825 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,825 INFO  L485      AbstractCegarLoop]: Abstraction has 61 states and 82 transitions.
[2025-04-28 21:21:32,825 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 8 states have (on average 2.125) internal successors, (17), 11 states have internal predecessors, (17), 4 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (8), 6 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:32,826 INFO  L278                IsEmpty]: Start isEmpty. Operand 61 states and 82 transitions.
[2025-04-28 21:21:32,827 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:32,827 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,827 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,827 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:32,827 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,828 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,828 INFO  L85        PathProgramCache]: Analyzing trace with hash -223402592, now seen corresponding path program 1 times
[2025-04-28 21:21:32,828 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,828 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [905815171]
[2025-04-28 21:21:32,828 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,829 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,834 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:32,843 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:32,843 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,843 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,064 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:33,064 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,065 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [905815171]
[2025-04-28 21:21:33,065 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [905815171] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,065 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,065 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [11] imperfect sequences [] total 11
[2025-04-28 21:21:33,065 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1921388305]
[2025-04-28 21:21:33,065 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,065 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:33,066 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,066 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:33,066 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=20, Invalid=90, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:33,067 INFO  L87              Difference]: Start difference. First operand 61 states and 82 transitions. Second operand  has 11 states, 8 states have (on average 2.125) internal successors, (17), 11 states have internal predecessors, (17), 4 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (8), 6 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:33,272 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,272 INFO  L93              Difference]: Finished difference Result 69 states and 90 transitions.
[2025-04-28 21:21:33,273 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:33,273 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 8 states have (on average 2.125) internal successors, (17), 11 states have internal predecessors, (17), 4 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (8), 6 states have call predecessors, (8), 4 states have call successors, (8) Word has length 33
[2025-04-28 21:21:33,274 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,274 INFO  L225             Difference]: With dead ends: 69
[2025-04-28 21:21:33,275 INFO  L226             Difference]: Without dead ends: 61
[2025-04-28 21:21:33,275 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=29, Invalid=127, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:33,276 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 4 mSDsluCounter, 267 mSDsCounter, 0 mSdLazyCounter, 151 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 307 SdHoareTripleChecker+Invalid, 151 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 151 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,276 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 307 Invalid, 151 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 151 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:33,277 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 61 states.
[2025-04-28 21:21:33,284 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 61 to 59.
[2025-04-28 21:21:33,285 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 59 states, 27 states have (on average 1.2962962962962963) internal successors, (35), 32 states have internal predecessors, (35), 14 states have call successors, (14), 9 states have call predecessors, (14), 17 states have return successors, (30), 17 states have call predecessors, (30), 14 states have call successors, (30)
[2025-04-28 21:21:33,286 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 59 states to 59 states and 79 transitions.
[2025-04-28 21:21:33,286 INFO  L79                 Accepts]: Start accepts. Automaton has 59 states and 79 transitions. Word has length 33
[2025-04-28 21:21:33,286 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,286 INFO  L485      AbstractCegarLoop]: Abstraction has 59 states and 79 transitions.
[2025-04-28 21:21:33,286 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 8 states have (on average 2.125) internal successors, (17), 11 states have internal predecessors, (17), 4 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (8), 6 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:33,287 INFO  L278                IsEmpty]: Start isEmpty. Operand 59 states and 79 transitions.
[2025-04-28 21:21:33,288 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:33,288 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,288 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,288 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:33,288 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,289 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,289 INFO  L85        PathProgramCache]: Analyzing trace with hash -1529994816, now seen corresponding path program 1 times
[2025-04-28 21:21:33,289 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,289 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1210748998]
[2025-04-28 21:21:33,289 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,289 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,294 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:33,300 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:33,300 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,300 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,541 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:33,542 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,542 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1210748998]
[2025-04-28 21:21:33,542 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1210748998] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,542 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2117222887]
[2025-04-28 21:21:33,542 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,542 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,545 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,548 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:33,551 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,637 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:33,660 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:33,660 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,660 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,663 INFO  L256         TraceCheckSpWp]: Trace formula consists of 119 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,664 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,926 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:33,927 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:36,498 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:36,498 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2117222887] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:36,498 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:36,498 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 11] total 22
[2025-04-28 21:21:36,499 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [945041136]
[2025-04-28 21:21:36,499 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,499 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:36,499 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,500 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:36,501 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=404, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:36,501 INFO  L87              Difference]: Start difference. First operand 59 states and 79 transitions. Second operand  has 22 states, 15 states have (on average 2.0) internal successors, (30), 22 states have internal predecessors, (30), 9 states have call successors, (13), 1 states have call predecessors, (13), 15 states have return successors, (18), 13 states have call predecessors, (18), 9 states have call successors, (18)
[2025-04-28 21:21:36,880 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,880 INFO  L93              Difference]: Finished difference Result 71 states and 92 transitions.
[2025-04-28 21:21:36,881 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:21:36,881 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 15 states have (on average 2.0) internal successors, (30), 22 states have internal predecessors, (30), 9 states have call successors, (13), 1 states have call predecessors, (13), 15 states have return successors, (18), 13 states have call predecessors, (18), 9 states have call successors, (18) Word has length 33
[2025-04-28 21:21:36,882 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,882 INFO  L225             Difference]: With dead ends: 71
[2025-04-28 21:21:36,883 INFO  L226             Difference]: Without dead ends: 71
[2025-04-28 21:21:36,883 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 82 GetRequests, 56 SyntacticMatches, 1 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 91 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=90, Invalid=612, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:36,884 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 7 mSDsluCounter, 396 mSDsCounter, 0 mSdLazyCounter, 276 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 430 SdHoareTripleChecker+Invalid, 283 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 276 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,884 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 430 Invalid, 283 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 276 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:36,885 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 71 states.
[2025-04-28 21:21:36,892 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 71 to 65.
[2025-04-28 21:21:36,893 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 65 states, 30 states have (on average 1.2666666666666666) internal successors, (38), 35 states have internal predecessors, (38), 14 states have call successors, (14), 9 states have call predecessors, (14), 20 states have return successors, (34), 20 states have call predecessors, (34), 14 states have call successors, (34)
[2025-04-28 21:21:36,894 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 65 states to 65 states and 86 transitions.
[2025-04-28 21:21:36,894 INFO  L79                 Accepts]: Start accepts. Automaton has 65 states and 86 transitions. Word has length 33
[2025-04-28 21:21:36,894 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,894 INFO  L485      AbstractCegarLoop]: Abstraction has 65 states and 86 transitions.
[2025-04-28 21:21:36,894 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 15 states have (on average 2.0) internal successors, (30), 22 states have internal predecessors, (30), 9 states have call successors, (13), 1 states have call predecessors, (13), 15 states have return successors, (18), 13 states have call predecessors, (18), 9 states have call successors, (18)
[2025-04-28 21:21:36,894 INFO  L278                IsEmpty]: Start isEmpty. Operand 65 states and 86 transitions.
[2025-04-28 21:21:36,896 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:36,896 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,896 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,902 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:37,100 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,100 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,101 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,101 INFO  L85        PathProgramCache]: Analyzing trace with hash -1335122081, now seen corresponding path program 1 times
[2025-04-28 21:21:37,101 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,101 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1100068556]
[2025-04-28 21:21:37,101 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,101 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,106 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:37,114 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:37,115 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,115 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,335 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:37,335 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,335 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1100068556]
[2025-04-28 21:21:37,335 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1100068556] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,335 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2121569877]
[2025-04-28 21:21:37,336 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,336 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,340 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,342 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:37,347 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,443 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:37,464 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:37,464 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,464 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,465 INFO  L256         TraceCheckSpWp]: Trace formula consists of 119 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,467 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,707 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:37,707 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,497 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:40,498 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2121569877] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,498 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,498 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 23
[2025-04-28 21:21:40,498 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1378192524]
[2025-04-28 21:21:40,498 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,498 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:40,499 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,499 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:40,499 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=60, Invalid=446, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:40,500 INFO  L87              Difference]: Start difference. First operand 65 states and 86 transitions. Second operand  has 23 states, 16 states have (on average 1.8125) internal successors, (29), 23 states have internal predecessors, (29), 8 states have call successors, (12), 1 states have call predecessors, (12), 15 states have return successors, (18), 13 states have call predecessors, (18), 8 states have call successors, (18)
[2025-04-28 21:21:40,810 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,810 INFO  L93              Difference]: Finished difference Result 77 states and 98 transitions.
[2025-04-28 21:21:40,811 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:40,811 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 16 states have (on average 1.8125) internal successors, (29), 23 states have internal predecessors, (29), 8 states have call successors, (12), 1 states have call predecessors, (12), 15 states have return successors, (18), 13 states have call predecessors, (18), 8 states have call successors, (18) Word has length 33
[2025-04-28 21:21:40,811 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,812 INFO  L225             Difference]: With dead ends: 77
[2025-04-28 21:21:40,812 INFO  L226             Difference]: Without dead ends: 77
[2025-04-28 21:21:40,813 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 81 GetRequests, 56 SyntacticMatches, 0 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 77 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=88, Invalid=614, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:40,813 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 4 mSDsluCounter, 567 mSDsCounter, 0 mSdLazyCounter, 290 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 609 SdHoareTripleChecker+Invalid, 297 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 290 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,814 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 609 Invalid, 297 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 290 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:40,814 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 77 states.
[2025-04-28 21:21:40,821 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 77 to 63.
[2025-04-28 21:21:40,821 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 63 states, 29 states have (on average 1.2758620689655173) internal successors, (37), 34 states have internal predecessors, (37), 14 states have call successors, (14), 9 states have call predecessors, (14), 19 states have return successors, (32), 19 states have call predecessors, (32), 14 states have call successors, (32)
[2025-04-28 21:21:40,822 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 63 states to 63 states and 83 transitions.
[2025-04-28 21:21:40,823 INFO  L79                 Accepts]: Start accepts. Automaton has 63 states and 83 transitions. Word has length 33
[2025-04-28 21:21:40,823 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,823 INFO  L485      AbstractCegarLoop]: Abstraction has 63 states and 83 transitions.
[2025-04-28 21:21:40,823 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 16 states have (on average 1.8125) internal successors, (29), 23 states have internal predecessors, (29), 8 states have call successors, (12), 1 states have call predecessors, (12), 15 states have return successors, (18), 13 states have call predecessors, (18), 8 states have call successors, (18)
[2025-04-28 21:21:40,823 INFO  L278                IsEmpty]: Start isEmpty. Operand 63 states and 83 transitions.
[2025-04-28 21:21:40,824 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:40,824 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,825 INFO  L218           NwaCegarLoop]: trace histogram [2, 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,831 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:41,029 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,029 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,030 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,030 INFO  L85        PathProgramCache]: Analyzing trace with hash -1245546523, now seen corresponding path program 1 times
[2025-04-28 21:21:41,030 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,030 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [326322120]
[2025-04-28 21:21:41,030 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,030 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,035 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:41,042 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:41,042 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,042 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,282 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:41,282 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,282 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [326322120]
[2025-04-28 21:21:41,283 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [326322120] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,283 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,283 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [13] imperfect sequences [] total 13
[2025-04-28 21:21:41,283 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [516750550]
[2025-04-28 21:21:41,283 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,283 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:41,283 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,284 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:41,284 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=131, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:41,284 INFO  L87              Difference]: Start difference. First operand 63 states and 83 transitions. Second operand  has 13 states, 9 states have (on average 2.111111111111111) internal successors, (19), 13 states have internal predecessors, (19), 5 states have call successors, (9), 1 states have call predecessors, (9), 8 states have return successors, (9), 7 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:41,545 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,545 INFO  L93              Difference]: Finished difference Result 73 states and 93 transitions.
[2025-04-28 21:21:41,546 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:41,546 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 9 states have (on average 2.111111111111111) internal successors, (19), 13 states have internal predecessors, (19), 5 states have call successors, (9), 1 states have call predecessors, (9), 8 states have return successors, (9), 7 states have call predecessors, (9), 5 states have call successors, (9) Word has length 37
[2025-04-28 21:21:41,547 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,547 INFO  L225             Difference]: With dead ends: 73
[2025-04-28 21:21:41,547 INFO  L226             Difference]: Without dead ends: 61
[2025-04-28 21:21:41,548 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 17 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 11 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=39, Invalid=201, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:41,548 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 5 mSDsluCounter, 361 mSDsCounter, 0 mSdLazyCounter, 233 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 405 SdHoareTripleChecker+Invalid, 233 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 233 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,550 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 405 Invalid, 233 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 233 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:41,550 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 61 states.
[2025-04-28 21:21:41,560 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 61 to 57.
[2025-04-28 21:21:41,560 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 57 states, 26 states have (on average 1.3076923076923077) internal successors, (34), 31 states have internal predecessors, (34), 14 states have call successors, (14), 9 states have call predecessors, (14), 16 states have return successors, (27), 16 states have call predecessors, (27), 14 states have call successors, (27)
[2025-04-28 21:21:41,561 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 57 states to 57 states and 75 transitions.
[2025-04-28 21:21:41,561 INFO  L79                 Accepts]: Start accepts. Automaton has 57 states and 75 transitions. Word has length 37
[2025-04-28 21:21:41,561 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,561 INFO  L485      AbstractCegarLoop]: Abstraction has 57 states and 75 transitions.
[2025-04-28 21:21:41,562 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 9 states have (on average 2.111111111111111) internal successors, (19), 13 states have internal predecessors, (19), 5 states have call successors, (9), 1 states have call predecessors, (9), 8 states have return successors, (9), 7 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:41,562 INFO  L278                IsEmpty]: Start isEmpty. Operand 57 states and 75 transitions.
[2025-04-28 21:21:41,562 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:41,562 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,567 INFO  L218           NwaCegarLoop]: trace histogram [2, 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,567 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:41,567 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,567 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,567 INFO  L85        PathProgramCache]: Analyzing trace with hash 1845075589, now seen corresponding path program 1 times
[2025-04-28 21:21:41,567 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,568 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [974646752]
[2025-04-28 21:21:41,568 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,568 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,574 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:41,582 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:41,585 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,585 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,808 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:41,808 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,808 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [974646752]
[2025-04-28 21:21:41,808 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [974646752] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,808 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1783028983]
[2025-04-28 21:21:41,809 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,809 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,811 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,814 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:41,816 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,936 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:41,953 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:41,953 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,953 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,954 INFO  L256         TraceCheckSpWp]: Trace formula consists of 138 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,956 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,162 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:42,162 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,533 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:45,534 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1783028983] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,534 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,534 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 13, 13] total 25
[2025-04-28 21:21:45,534 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1872789772]
[2025-04-28 21:21:45,534 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,535 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:21:45,535 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,535 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:21:45,536 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=66, Invalid=534, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:45,536 INFO  L87              Difference]: Start difference. First operand 57 states and 75 transitions. Second operand  has 25 states, 16 states have (on average 2.125) internal successors, (34), 25 states have internal predecessors, (34), 11 states have call successors, (16), 1 states have call predecessors, (16), 16 states have return successors, (21), 14 states have call predecessors, (21), 11 states have call successors, (21)
[2025-04-28 21:21:45,999 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,999 INFO  L93              Difference]: Finished difference Result 69 states and 88 transitions.
[2025-04-28 21:21:46,000 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 19 states. 
[2025-04-28 21:21:46,000 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 16 states have (on average 2.125) internal successors, (34), 25 states have internal predecessors, (34), 11 states have call successors, (16), 1 states have call predecessors, (16), 16 states have return successors, (21), 14 states have call predecessors, (21), 11 states have call successors, (21) Word has length 37
[2025-04-28 21:21:46,000 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,001 INFO  L225             Difference]: With dead ends: 69
[2025-04-28 21:21:46,001 INFO  L226             Difference]: Without dead ends: 69
[2025-04-28 21:21:46,001 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 92 GetRequests, 60 SyntacticMatches, 3 SemanticMatches, 29 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 138 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=105, Invalid=825, Unknown=0, NotChecked=0, Total=930
[2025-04-28 21:21:46,002 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 6 mSDsluCounter, 552 mSDsCounter, 0 mSdLazyCounter, 373 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 592 SdHoareTripleChecker+Invalid, 379 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 373 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,002 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 592 Invalid, 379 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 373 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:46,003 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 69 states.
[2025-04-28 21:21:46,009 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 69 to 55.
[2025-04-28 21:21:46,009 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 55 states, 25 states have (on average 1.32) internal successors, (33), 30 states have internal predecessors, (33), 14 states have call successors, (14), 9 states have call predecessors, (14), 15 states have return successors, (26), 15 states have call predecessors, (26), 14 states have call successors, (26)
[2025-04-28 21:21:46,010 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 55 states to 55 states and 73 transitions.
[2025-04-28 21:21:46,010 INFO  L79                 Accepts]: Start accepts. Automaton has 55 states and 73 transitions. Word has length 37
[2025-04-28 21:21:46,010 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,010 INFO  L485      AbstractCegarLoop]: Abstraction has 55 states and 73 transitions.
[2025-04-28 21:21:46,011 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 16 states have (on average 2.125) internal successors, (34), 25 states have internal predecessors, (34), 11 states have call successors, (16), 1 states have call predecessors, (16), 16 states have return successors, (21), 14 states have call predecessors, (21), 11 states have call successors, (21)
[2025-04-28 21:21:46,011 INFO  L278                IsEmpty]: Start isEmpty. Operand 55 states and 73 transitions.
[2025-04-28 21:21:46,011 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:46,012 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,012 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, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,020 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:46,212 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:46,212 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,213 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,213 INFO  L85        PathProgramCache]: Analyzing trace with hash -560095323, now seen corresponding path program 2 times
[2025-04-28 21:21:46,213 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,213 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [76696764]
[2025-04-28 21:21:46,213 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,213 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,221 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 37 statements into 2 equivalence classes.
[2025-04-28 21:21:46,223 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 1 check-sat command(s) and asserted 25 of 37 statements.
[2025-04-28 21:21:46,224 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 1 check-sat command(s)
[2025-04-28 21:21:46,224 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,250 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:46,250 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,251 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [76696764]
[2025-04-28 21:21:46,251 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [76696764] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,251 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,251 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:46,251 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [851420425]
[2025-04-28 21:21:46,251 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,251 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:46,252 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,252 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:46,252 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,252 INFO  L87              Difference]: Start difference. First operand 55 states and 73 transitions. Second operand  has 4 states, 3 states have (on average 5.0) internal successors, (15), 4 states have internal predecessors, (15), 2 states have call successors, (8), 1 states have call predecessors, (8), 2 states have return successors, (8), 1 states have call predecessors, (8), 2 states have call successors, (8)
[2025-04-28 21:21:46,280 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,280 INFO  L93              Difference]: Finished difference Result 55 states and 72 transitions.
[2025-04-28 21:21:46,281 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:46,281 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 5.0) internal successors, (15), 4 states have internal predecessors, (15), 2 states have call successors, (8), 1 states have call predecessors, (8), 2 states have return successors, (8), 1 states have call predecessors, (8), 2 states have call successors, (8) Word has length 37
[2025-04-28 21:21:46,281 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,282 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:46,282 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:46,282 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,283 INFO  L437           NwaCegarLoop]: 37 mSDtfsCounter, 1 mSDsluCounter, 65 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 102 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,283 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 102 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:46,284 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:46,288 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 55.
[2025-04-28 21:21:46,289 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 55 states, 25 states have (on average 1.32) internal successors, (33), 30 states have internal predecessors, (33), 14 states have call successors, (14), 9 states have call predecessors, (14), 15 states have return successors, (25), 15 states have call predecessors, (25), 14 states have call successors, (25)
[2025-04-28 21:21:46,289 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 55 states to 55 states and 72 transitions.
[2025-04-28 21:21:46,290 INFO  L79                 Accepts]: Start accepts. Automaton has 55 states and 72 transitions. Word has length 37
[2025-04-28 21:21:46,290 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,290 INFO  L485      AbstractCegarLoop]: Abstraction has 55 states and 72 transitions.
[2025-04-28 21:21:46,290 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 5.0) internal successors, (15), 4 states have internal predecessors, (15), 2 states have call successors, (8), 1 states have call predecessors, (8), 2 states have return successors, (8), 1 states have call predecessors, (8), 2 states have call successors, (8)
[2025-04-28 21:21:46,290 INFO  L278                IsEmpty]: Start isEmpty. Operand 55 states and 72 transitions.
[2025-04-28 21:21:46,291 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:46,291 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,291 INFO  L218           NwaCegarLoop]: trace histogram [2, 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, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,291 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:46,292 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,292 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,292 INFO  L85        PathProgramCache]: Analyzing trace with hash 1746774276, now seen corresponding path program 1 times
[2025-04-28 21:21:46,292 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,292 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1098714905]
[2025-04-28 21:21:46,292 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,293 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,299 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:46,306 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:46,306 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,306 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,563 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:46,563 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,563 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1098714905]
[2025-04-28 21:21:46,563 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1098714905] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,564 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1398879904]
[2025-04-28 21:21:46,564 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,564 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,567 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,569 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:46,578 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,740 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:46,756 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:46,756 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,756 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,757 INFO  L256         TraceCheckSpWp]: Trace formula consists of 138 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,758 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,995 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:46,995 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
