./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-220.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:25,183 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:25,265 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bce16337-47ba-407c-965f-82f1adc093bb/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:25,274 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:25,274 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:25,314 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:25,315 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:25,315 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:25,316 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:25,317 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:25,317 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:25,318 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:25,318 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:25,318 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:25,319 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:25,319 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:25,319 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:25,319 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:25,319 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:25,319 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:25,320 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:25,320 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:25,320 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:25,321 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:25,321 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:25,321 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:25,322 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:25,671 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:25,683 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:25,686 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:25,689 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:25,690 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:25,691 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bce16337-47ba-407c-965f-82f1adc093bb/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-220.smt2
[2025-04-28 21:21:25,694 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:25,698 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:26,147 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bce16337-47ba-407c-965f-82f1adc093bb/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-220.smt2
[2025-04-28 21:21:26,150 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:26,152 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:26,153 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:26,153 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:26,153 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:26,156 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,199 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26 Unit
[2025-04-28 21:21:26,199 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:26,200 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:26,200 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:26,200 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:26,218 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,218 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,248 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,248 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,254 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,256 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,260 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,262 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,263 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,277 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:26,278 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:26,278 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:26,278 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:26,279 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (1/1) ...
[2025-04-28 21:21:26,286 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:26,304 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:26,320 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:26,324 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:26,337 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:26,337 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:26,337 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:26,338 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Inv given in one single declaration
[2025-04-28 21:21:26,338 INFO  L130     BoogieDeclarations]: Found specification of procedure Inv
[2025-04-28 21:21:26,338 INFO  L138     BoogieDeclarations]: Found implementation of procedure Inv
[2025-04-28 21:21:26,338 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:26,338 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:26,338 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:26,412 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:26,415 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:26,899 INFO  L?                        ?]: Removed 11 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:26,899 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:26,922 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:26,925 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:26,927 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:26 BoogieIcfgContainer
[2025-04-28 21:21:26,928 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:26,930 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:26,932 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:26,937 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:26,937 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:26" (1/3) ...
[2025-04-28 21:21:26,939 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@14eac822 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:26, skipping insertion in model container
[2025-04-28 21:21:26,939 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:26" (2/3) ...
[2025-04-28 21:21:26,940 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@14eac822 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:26, skipping insertion in model container
[2025-04-28 21:21:26,940 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:26" (3/3) ...
[2025-04-28 21:21:26,942 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:26,971 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:26,974 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 58 locations, 197 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:27,035 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:27,054 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;@15e3e2f1, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:27,056 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:27,061 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 58 states, 6 states have (on average 8.333333333333334) internal successors, (50), 50 states have internal predecessors, (50), 49 states have call successors, (49), 2 states have call predecessors, (49), 2 states have return successors, (49), 7 states have call predecessors, (49), 49 states have call successors, (49)
[2025-04-28 21:21:27,107 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-04-28 21:21:27,107 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,108 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-04-28 21:21:27,108 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,114 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,115 INFO  L85        PathProgramCache]: Analyzing trace with hash 337616417, now seen corresponding path program 1 times
[2025-04-28 21:21:27,125 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,125 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1915164762]
[2025-04-28 21:21:27,126 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,127 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,152 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-04-28 21:21:27,155 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-04-28 21:21:27,155 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,156 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,192 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:27,193 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,193 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1915164762]
[2025-04-28 21:21:27,194 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1915164762] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,194 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,198 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-04-28 21:21:27,201 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1749692802]
[2025-04-28 21:21:27,203 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,207 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-04-28 21:21:27,210 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,251 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-04-28 21:21:27,252 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:27,255 INFO  L87              Difference]: Start difference. First operand  has 58 states, 6 states have (on average 8.333333333333334) internal successors, (50), 50 states have internal predecessors, (50), 49 states have call successors, (49), 2 states have call predecessors, (49), 2 states have return successors, (49), 7 states have call predecessors, (49), 49 states have call successors, (49) Second operand  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:27,301 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,302 INFO  L93              Difference]: Finished difference Result 56 states and 145 transitions.
[2025-04-28 21:21:27,303 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-04-28 21:21:27,304 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1) Word has length 5
[2025-04-28 21:21:27,304 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,317 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:27,317 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:27,319 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:27,323 INFO  L437           NwaCegarLoop]: 145 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 145 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,324 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 145 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:27,343 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:27,389 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 56.
[2025-04-28 21:21:27,391 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 5 states have (on average 9.4) internal successors, (47), 47 states have internal predecessors, (47), 49 states have call successors, (49), 2 states have call predecessors, (49), 2 states have return successors, (49), 7 states have call predecessors, (49), 49 states have call successors, (49)
[2025-04-28 21:21:27,403 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 145 transitions.
[2025-04-28 21:21:27,405 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 145 transitions. Word has length 5
[2025-04-28 21:21:27,405 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,405 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 145 transitions.
[2025-04-28 21:21:27,405 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-04-28 21:21:27,405 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 145 transitions.
[2025-04-28 21:21:27,426 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:27,427 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,427 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,428 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:27,428 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,429 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,429 INFO  L85        PathProgramCache]: Analyzing trace with hash 2060133119, now seen corresponding path program 1 times
[2025-04-28 21:21:27,430 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,430 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [487807134]
[2025-04-28 21:21:27,430 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,430 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,438 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:27,495 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:27,495 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,495 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,627 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:27,627 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,627 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [487807134]
[2025-04-28 21:21:27,627 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [487807134] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:27,627 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:27,627 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:27,628 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1151929856]
[2025-04-28 21:21:27,628 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,629 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:27,629 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,633 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:27,633 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:27,633 INFO  L87              Difference]: Start difference. First operand 56 states and 145 transitions. Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:28,752 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,753 INFO  L93              Difference]: Finished difference Result 92 states and 294 transitions.
[2025-04-28 21:21:28,753 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:28,754 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:28,754 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,772 INFO  L225             Difference]: With dead ends: 92
[2025-04-28 21:21:28,773 INFO  L226             Difference]: Without dead ends: 92
[2025-04-28 21:21:28,773 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,774 INFO  L437           NwaCegarLoop]: 161 mSDtfsCounter, 30 mSDsluCounter, 192 mSDsCounter, 0 mSdLazyCounter, 273 mSolverCounterSat, 75 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 37 SdHoareTripleChecker+Valid, 353 SdHoareTripleChecker+Invalid, 348 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 75 IncrementalHoareTripleChecker+Valid, 273 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,778 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [37 Valid, 353 Invalid, 348 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [75 Valid, 273 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:21:28,779 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-04-28 21:21:28,838 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 92.
[2025-04-28 21:21:28,839 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 7 states have (on average 11.142857142857142) internal successors, (78), 77 states have internal predecessors, (78), 83 states have call successors, (83), 3 states have call predecessors, (83), 3 states have return successors, (133), 12 states have call predecessors, (133), 83 states have call successors, (133)
[2025-04-28 21:21:28,848 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 294 transitions.
[2025-04-28 21:21:28,849 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 294 transitions. Word has length 9
[2025-04-28 21:21:28,850 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,850 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 294 transitions.
[2025-04-28 21:21:28,851 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:28,851 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 294 transitions.
[2025-04-28 21:21:28,868 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:28,868 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,868 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,868 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:28,869 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,870 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,870 INFO  L85        PathProgramCache]: Analyzing trace with hash 208086214, now seen corresponding path program 1 times
[2025-04-28 21:21:28,870 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,871 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1563829124]
[2025-04-28 21:21:28,871 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,871 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,884 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:28,901 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:28,901 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,901 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,025 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,025 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,025 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1563829124]
[2025-04-28 21:21:29,025 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1563829124] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,025 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1639254223]
[2025-04-28 21:21:29,026 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,026 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,030 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,036 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:29,038 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,089 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:29,111 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:29,111 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,111 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,114 INFO  L256         TraceCheckSpWp]: Trace formula consists of 98 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,119 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,203 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,204 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:29,396 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,396 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1639254223] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:29,396 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:29,396 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 5
[2025-04-28 21:21:29,397 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1588856004]
[2025-04-28 21:21:29,397 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,397 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:29,397 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,398 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:29,398 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:29,398 INFO  L87              Difference]: Start difference. First operand 92 states and 294 transitions. Second operand  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:31,643 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,643 INFO  L93              Difference]: Finished difference Result 249 states and 1211 transitions.
[2025-04-28 21:21:31,644 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:31,644 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:31,645 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,684 INFO  L225             Difference]: With dead ends: 249
[2025-04-28 21:21:31,684 INFO  L226             Difference]: Without dead ends: 249
[2025-04-28 21:21:31,684 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 30 GetRequests, 23 SyntacticMatches, 3 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:31,686 INFO  L437           NwaCegarLoop]: 186 mSDtfsCounter, 130 mSDsluCounter, 275 mSDsCounter, 0 mSdLazyCounter, 706 mSolverCounterSat, 322 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 147 SdHoareTripleChecker+Valid, 461 SdHoareTripleChecker+Invalid, 1028 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 322 IncrementalHoareTripleChecker+Valid, 706 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,687 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [147 Valid, 461 Invalid, 1028 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [322 Valid, 706 Invalid, 0 Unknown, 0 Unchecked, 2.1s Time]
[2025-04-28 21:21:31,689 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 249 states.
[2025-04-28 21:21:31,840 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 249 to 177.
[2025-04-28 21:21:31,842 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 177 states, 11 states have (on average 13.909090909090908) internal successors, (153), 150 states have internal predecessors, (153), 164 states have call successors, (164), 5 states have call predecessors, (164), 5 states have return successors, (399), 22 states have call predecessors, (399), 164 states have call successors, (399)
[2025-04-28 21:21:31,852 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 177 states to 177 states and 716 transitions.
[2025-04-28 21:21:31,853 INFO  L79                 Accepts]: Start accepts. Automaton has 177 states and 716 transitions. Word has length 12
[2025-04-28 21:21:31,853 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,854 INFO  L485      AbstractCegarLoop]: Abstraction has 177 states and 716 transitions.
[2025-04-28 21:21:31,854 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:31,854 INFO  L278                IsEmpty]: Start isEmpty. Operand 177 states and 716 transitions.
[2025-04-28 21:21:31,872 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:31,872 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,873 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,880 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:32,074 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,075 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,075 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,075 INFO  L85        PathProgramCache]: Analyzing trace with hash -623401613, now seen corresponding path program 1 times
[2025-04-28 21:21:32,075 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,076 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [61678806]
[2025-04-28 21:21:32,076 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,076 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,081 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:32,085 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:32,085 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,086 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,147 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,149 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,150 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [61678806]
[2025-04-28 21:21:32,150 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [61678806] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,150 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:32,150 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:32,150 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1748930339]
[2025-04-28 21:21:32,150 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,150 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:32,150 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,151 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:32,151 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:32,151 INFO  L87              Difference]: Start difference. First operand 177 states and 716 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:32,836 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,836 INFO  L93              Difference]: Finished difference Result 321 states and 1622 transitions.
[2025-04-28 21:21:32,836 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:32,837 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-04-28 21:21:32,837 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,876 INFO  L225             Difference]: With dead ends: 321
[2025-04-28 21:21:32,877 INFO  L226             Difference]: Without dead ends: 321
[2025-04-28 21:21:32,877 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:32,878 INFO  L437           NwaCegarLoop]: 212 mSDtfsCounter, 30 mSDsluCounter, 254 mSDsCounter, 0 mSdLazyCounter, 275 mSolverCounterSat, 75 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 466 SdHoareTripleChecker+Invalid, 350 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 75 IncrementalHoareTripleChecker+Valid, 275 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,878 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 466 Invalid, 350 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [75 Valid, 275 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:32,879 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 321 states.
[2025-04-28 21:21:33,032 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 321 to 321.
[2025-04-28 21:21:33,034 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 321 states, 19 states have (on average 14.578947368421053) internal successors, (277), 270 states have internal predecessors, (277), 300 states have call successors, (300), 9 states have call predecessors, (300), 9 states have return successors, (1045), 42 states have call predecessors, (1045), 300 states have call successors, (1045)
[2025-04-28 21:21:33,049 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 321 states to 321 states and 1622 transitions.
[2025-04-28 21:21:33,049 INFO  L79                 Accepts]: Start accepts. Automaton has 321 states and 1622 transitions. Word has length 13
[2025-04-28 21:21:33,050 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,050 INFO  L485      AbstractCegarLoop]: Abstraction has 321 states and 1622 transitions.
[2025-04-28 21:21:33,050 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:33,050 INFO  L278                IsEmpty]: Start isEmpty. Operand 321 states and 1622 transitions.
[2025-04-28 21:21:33,069 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:33,070 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,070 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,070 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:33,070 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,071 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,071 INFO  L85        PathProgramCache]: Analyzing trace with hash 771138058, now seen corresponding path program 1 times
[2025-04-28 21:21:33,071 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,071 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1880084824]
[2025-04-28 21:21:33,071 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,071 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,077 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:33,094 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:33,094 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,094 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,148 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:33,148 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,148 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1880084824]
[2025-04-28 21:21:33,148 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1880084824] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:33,148 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:33,148 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:33,148 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [823721971]
[2025-04-28 21:21:33,149 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,149 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:33,149 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,149 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:33,149 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:33,150 INFO  L87              Difference]: Start difference. First operand 321 states and 1622 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:33,841 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,841 INFO  L93              Difference]: Finished difference Result 465 states and 2792 transitions.
[2025-04-28 21:21:33,842 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:33,842 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-04-28 21:21:33,843 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,903 INFO  L225             Difference]: With dead ends: 465
[2025-04-28 21:21:33,903 INFO  L226             Difference]: Without dead ends: 465
[2025-04-28 21:21:33,904 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:33,905 INFO  L437           NwaCegarLoop]: 212 mSDtfsCounter, 30 mSDsluCounter, 240 mSDsCounter, 0 mSdLazyCounter, 282 mSolverCounterSat, 75 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 43 SdHoareTripleChecker+Valid, 452 SdHoareTripleChecker+Invalid, 357 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 75 IncrementalHoareTripleChecker+Valid, 282 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,906 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [43 Valid, 452 Invalid, 357 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [75 Valid, 282 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:33,907 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 465 states.
[2025-04-28 21:21:34,183 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 465 to 465.
[2025-04-28 21:21:34,186 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 465 states, 27 states have (on average 15.37037037037037) internal successors, (415), 390 states have internal predecessors, (415), 436 states have call successors, (436), 13 states have call predecessors, (436), 13 states have return successors, (1941), 62 states have call predecessors, (1941), 436 states have call successors, (1941)
[2025-04-28 21:21:34,215 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 465 states to 465 states and 2792 transitions.
[2025-04-28 21:21:34,215 INFO  L79                 Accepts]: Start accepts. Automaton has 465 states and 2792 transitions. Word has length 13
[2025-04-28 21:21:34,216 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,216 INFO  L485      AbstractCegarLoop]: Abstraction has 465 states and 2792 transitions.
[2025-04-28 21:21:34,216 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:34,216 INFO  L278                IsEmpty]: Start isEmpty. Operand 465 states and 2792 transitions.
[2025-04-28 21:21:34,240 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:34,240 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,240 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,240 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:34,240 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,242 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,242 INFO  L85        PathProgramCache]: Analyzing trace with hash 1387342559, now seen corresponding path program 1 times
[2025-04-28 21:21:34,242 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,242 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [660792670]
[2025-04-28 21:21:34,242 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,243 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,252 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:34,257 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:34,257 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,257 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,320 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:34,321 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,321 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [660792670]
[2025-04-28 21:21:34,321 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [660792670] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:34,321 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:34,321 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:34,321 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [514158534]
[2025-04-28 21:21:34,321 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,321 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:34,322 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,322 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:34,322 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:34,322 INFO  L87              Difference]: Start difference. First operand 465 states and 2792 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:34,975 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,976 INFO  L93              Difference]: Finished difference Result 609 states and 4218 transitions.
[2025-04-28 21:21:34,976 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:34,977 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-04-28 21:21:34,977 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,088 INFO  L225             Difference]: With dead ends: 609
[2025-04-28 21:21:35,089 INFO  L226             Difference]: Without dead ends: 609
[2025-04-28 21:21:35,089 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:35,089 INFO  L437           NwaCegarLoop]: 212 mSDtfsCounter, 30 mSDsluCounter, 234 mSDsCounter, 0 mSdLazyCounter, 287 mSolverCounterSat, 75 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 46 SdHoareTripleChecker+Valid, 446 SdHoareTripleChecker+Invalid, 362 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 75 IncrementalHoareTripleChecker+Valid, 287 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,090 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [46 Valid, 446 Invalid, 362 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [75 Valid, 287 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:35,091 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 609 states.
[2025-04-28 21:21:35,583 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 609 to 609.
[2025-04-28 21:21:35,588 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 609 states, 35 states have (on average 15.971428571428572) internal successors, (559), 510 states have internal predecessors, (559), 572 states have call successors, (572), 17 states have call predecessors, (572), 17 states have return successors, (3087), 82 states have call predecessors, (3087), 572 states have call successors, (3087)
[2025-04-28 21:21:35,646 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 609 states to 609 states and 4218 transitions.
[2025-04-28 21:21:35,646 INFO  L79                 Accepts]: Start accepts. Automaton has 609 states and 4218 transitions. Word has length 13
[2025-04-28 21:21:35,646 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,646 INFO  L485      AbstractCegarLoop]: Abstraction has 609 states and 4218 transitions.
[2025-04-28 21:21:35,647 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:35,647 INFO  L278                IsEmpty]: Start isEmpty. Operand 609 states and 4218 transitions.
[2025-04-28 21:21:35,683 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:35,683 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,683 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,683 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:35,683 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,684 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,684 INFO  L85        PathProgramCache]: Analyzing trace with hash -1436119619, now seen corresponding path program 1 times
[2025-04-28 21:21:35,684 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,685 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1057904768]
[2025-04-28 21:21:35,685 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,685 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,691 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:35,696 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:35,696 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,696 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,756 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:35,756 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,756 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1057904768]
[2025-04-28 21:21:35,756 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1057904768] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,756 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:35,756 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:35,756 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1965451657]
[2025-04-28 21:21:35,757 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,757 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:35,757 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,757 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:35,758 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:35,758 INFO  L87              Difference]: Start difference. First operand 609 states and 4218 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:36,919 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,919 INFO  L93              Difference]: Finished difference Result 717 states and 8368 transitions.
[2025-04-28 21:21:36,920 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:36,920 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 13
[2025-04-28 21:21:36,920 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,271 INFO  L225             Difference]: With dead ends: 717
[2025-04-28 21:21:37,271 INFO  L226             Difference]: Without dead ends: 717
[2025-04-28 21:21:37,272 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:37,272 INFO  L437           NwaCegarLoop]: 172 mSDtfsCounter, 31 mSDsluCounter, 173 mSDsCounter, 0 mSdLazyCounter, 426 mSolverCounterSat, 76 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 64 SdHoareTripleChecker+Valid, 345 SdHoareTripleChecker+Invalid, 502 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 76 IncrementalHoareTripleChecker+Valid, 426 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,273 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [64 Valid, 345 Invalid, 502 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [76 Valid, 426 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:21:37,274 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 717 states.
[2025-04-28 21:21:38,087 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 717 to 681.
[2025-04-28 21:21:38,091 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 681 states, 39 states have (on average 15.923076923076923) internal successors, (621), 570 states have internal predecessors, (621), 640 states have call successors, (640), 19 states have call predecessors, (640), 19 states have return successors, (3545), 92 states have call predecessors, (3545), 640 states have call successors, (3545)
[2025-04-28 21:21:38,136 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 681 states to 681 states and 4806 transitions.
[2025-04-28 21:21:38,136 INFO  L79                 Accepts]: Start accepts. Automaton has 681 states and 4806 transitions. Word has length 13
[2025-04-28 21:21:38,136 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,136 INFO  L485      AbstractCegarLoop]: Abstraction has 681 states and 4806 transitions.
[2025-04-28 21:21:38,137 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:38,137 INFO  L278                IsEmpty]: Start isEmpty. Operand 681 states and 4806 transitions.
[2025-04-28 21:21:38,189 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:38,189 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,189 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,189 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:38,190 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,190 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,191 INFO  L85        PathProgramCache]: Analyzing trace with hash 1537233664, now seen corresponding path program 1 times
[2025-04-28 21:21:38,191 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,191 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [609126349]
[2025-04-28 21:21:38,191 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,191 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,195 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:38,199 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:38,199 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,199 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,249 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:38,249 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,249 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [609126349]
[2025-04-28 21:21:38,249 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [609126349] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:38,249 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2141896772]
[2025-04-28 21:21:38,249 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,249 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,252 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:38,254 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:38,259 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:38,297 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:38,345 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:38,345 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,345 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,346 INFO  L256         TraceCheckSpWp]: Trace formula consists of 143 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:38,348 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:38,371 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:38,372 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,566 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:38,566 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2141896772] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,566 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,566 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-04-28 21:21:38,566 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [454246521]
[2025-04-28 21:21:38,566 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,567 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:38,567 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,567 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:38,568 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:38,568 INFO  L87              Difference]: Start difference. First operand 681 states and 4806 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:42,282 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,283 INFO  L93              Difference]: Finished difference Result 753 states and 11327 transitions.
[2025-04-28 21:21:42,283 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:42,283 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 16
[2025-04-28 21:21:42,283 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,631 INFO  L225             Difference]: With dead ends: 753
[2025-04-28 21:21:42,631 INFO  L226             Difference]: Without dead ends: 753
[2025-04-28 21:21:42,631 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 44 GetRequests, 31 SyntacticMatches, 2 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 20 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=54, Invalid=102, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:42,632 INFO  L437           NwaCegarLoop]: 199 mSDtfsCounter, 137 mSDsluCounter, 311 mSDsCounter, 0 mSdLazyCounter, 1342 mSolverCounterSat, 343 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 3.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 269 SdHoareTripleChecker+Valid, 510 SdHoareTripleChecker+Invalid, 1685 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 343 IncrementalHoareTripleChecker+Valid, 1342 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 3.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,632 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [269 Valid, 510 Invalid, 1685 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [343 Valid, 1342 Invalid, 0 Unknown, 0 Unchecked, 3.4s Time]
[2025-04-28 21:21:42,634 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 753 states.
[2025-04-28 21:21:43,775 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 753 to 609.
[2025-04-28 21:21:43,779 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 609 states, 35 states have (on average 15.971428571428572) internal successors, (559), 510 states have internal predecessors, (559), 572 states have call successors, (572), 17 states have call predecessors, (572), 17 states have return successors, (2919), 82 states have call predecessors, (2919), 572 states have call successors, (2919)
[2025-04-28 21:21:43,814 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 609 states to 609 states and 4050 transitions.
[2025-04-28 21:21:43,814 INFO  L79                 Accepts]: Start accepts. Automaton has 609 states and 4050 transitions. Word has length 16
[2025-04-28 21:21:43,815 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,815 INFO  L485      AbstractCegarLoop]: Abstraction has 609 states and 4050 transitions.
[2025-04-28 21:21:43,815 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:43,815 INFO  L278                IsEmpty]: Start isEmpty. Operand 609 states and 4050 transitions.
[2025-04-28 21:21:43,840 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:43,840 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,841 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,846 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:44,041 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,041 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,044 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,045 INFO  L85        PathProgramCache]: Analyzing trace with hash -2041679230, now seen corresponding path program 1 times
[2025-04-28 21:21:44,047 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,047 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1698674710]
[2025-04-28 21:21:44,047 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,047 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,054 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:44,059 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:44,060 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,061 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,112 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:44,112 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,112 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1698674710]
[2025-04-28 21:21:44,112 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1698674710] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,112 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,112 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:44,113 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2106121526]
[2025-04-28 21:21:44,113 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,113 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:44,113 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,113 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:44,113 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:44,114 INFO  L87              Difference]: Start difference. First operand 609 states and 4050 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:45,085 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,085 INFO  L93              Difference]: Finished difference Result 793 states and 9036 transitions.
[2025-04-28 21:21:45,085 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:45,086 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:21:45,086 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,246 INFO  L225             Difference]: With dead ends: 793
[2025-04-28 21:21:45,246 INFO  L226             Difference]: Without dead ends: 793
[2025-04-28 21:21:45,246 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:45,247 INFO  L437           NwaCegarLoop]: 166 mSDtfsCounter, 31 mSDsluCounter, 152 mSDsCounter, 0 mSdLazyCounter, 405 mSolverCounterSat, 95 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 85 SdHoareTripleChecker+Valid, 318 SdHoareTripleChecker+Invalid, 500 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 95 IncrementalHoareTripleChecker+Valid, 405 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,247 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [85 Valid, 318 Invalid, 500 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [95 Valid, 405 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:45,248 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 793 states.
[2025-04-28 21:21:45,847 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 793 to 753.
[2025-04-28 21:21:45,852 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 753 states, 43 states have (on average 16.209302325581394) internal successors, (697), 630 states have internal predecessors, (697), 708 states have call successors, (708), 21 states have call predecessors, (708), 21 states have return successors, (3806), 102 states have call predecessors, (3806), 708 states have call successors, (3806)
[2025-04-28 21:21:45,902 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 753 states to 753 states and 5211 transitions.
[2025-04-28 21:21:45,903 INFO  L79                 Accepts]: Start accepts. Automaton has 753 states and 5211 transitions. Word has length 17
[2025-04-28 21:21:45,903 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,903 INFO  L485      AbstractCegarLoop]: Abstraction has 753 states and 5211 transitions.
[2025-04-28 21:21:45,903 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:45,903 INFO  L278                IsEmpty]: Start isEmpty. Operand 753 states and 5211 transitions.
[2025-04-28 21:21:45,976 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:45,976 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,976 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,976 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:45,977 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,978 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,979 INFO  L85        PathProgramCache]: Analyzing trace with hash 1018317048, now seen corresponding path program 1 times
[2025-04-28 21:21:45,979 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,979 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [765886919]
[2025-04-28 21:21:45,979 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,979 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,986 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:45,993 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:45,993 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,993 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,044 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:46,045 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,045 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [765886919]
[2025-04-28 21:21:46,045 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [765886919] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,045 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,045 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:46,045 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1149195699]
[2025-04-28 21:21:46,045 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,045 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:46,045 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,046 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:46,046 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,046 INFO  L87              Difference]: Start difference. First operand 753 states and 5211 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:46,984 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,984 INFO  L93              Difference]: Finished difference Result 869 states and 10232 transitions.
[2025-04-28 21:21:46,984 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:46,985 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 19
[2025-04-28 21:21:46,985 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,245 INFO  L225             Difference]: With dead ends: 869
[2025-04-28 21:21:47,245 INFO  L226             Difference]: Without dead ends: 869
[2025-04-28 21:21:47,246 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:47,247 INFO  L437           NwaCegarLoop]: 194 mSDtfsCounter, 31 mSDsluCounter, 261 mSDsCounter, 0 mSdLazyCounter, 390 mSolverCounterSat, 64 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 41 SdHoareTripleChecker+Valid, 455 SdHoareTripleChecker+Invalid, 454 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 64 IncrementalHoareTripleChecker+Valid, 390 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,247 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [41 Valid, 455 Invalid, 454 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [64 Valid, 390 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:47,249 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 869 states.
[2025-04-28 21:21:48,197 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 869 to 825.
[2025-04-28 21:21:48,202 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 825 states, 47 states have (on average 16.148936170212767) internal successors, (759), 690 states have internal predecessors, (759), 776 states have call successors, (776), 23 states have call predecessors, (776), 23 states have return successors, (4338), 112 states have call predecessors, (4338), 776 states have call successors, (4338)
[2025-04-28 21:21:48,266 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 825 states to 825 states and 5873 transitions.
[2025-04-28 21:21:48,269 INFO  L79                 Accepts]: Start accepts. Automaton has 825 states and 5873 transitions. Word has length 19
[2025-04-28 21:21:48,269 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,269 INFO  L485      AbstractCegarLoop]: Abstraction has 825 states and 5873 transitions.
[2025-04-28 21:21:48,270 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:48,270 INFO  L278                IsEmpty]: Start isEmpty. Operand 825 states and 5873 transitions.
[2025-04-28 21:21:48,309 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:48,309 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,309 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,309 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:48,309 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,310 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,310 INFO  L85        PathProgramCache]: Analyzing trace with hash 1805658195, now seen corresponding path program 1 times
[2025-04-28 21:21:48,310 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,310 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [32609764]
[2025-04-28 21:21:48,310 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,310 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,315 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:48,319 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:48,319 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,319 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,364 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:48,364 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,364 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [32609764]
[2025-04-28 21:21:48,364 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [32609764] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,364 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,364 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:48,364 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1918115884]
[2025-04-28 21:21:48,364 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,365 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:48,365 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,365 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:48,365 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:48,365 INFO  L87              Difference]: Start difference. First operand 825 states and 5873 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:49,059 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,059 INFO  L93              Difference]: Finished difference Result 1091 states and 16008 transitions.
[2025-04-28 21:21:49,060 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:49,060 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 19
[2025-04-28 21:21:49,060 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,560 INFO  L225             Difference]: With dead ends: 1091
[2025-04-28 21:21:49,561 INFO  L226             Difference]: Without dead ends: 1091
[2025-04-28 21:21:49,561 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:49,562 INFO  L437           NwaCegarLoop]: 184 mSDtfsCounter, 15 mSDsluCounter, 185 mSDsCounter, 0 mSdLazyCounter, 289 mSolverCounterSat, 74 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 369 SdHoareTripleChecker+Invalid, 363 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 74 IncrementalHoareTripleChecker+Valid, 289 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,562 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 369 Invalid, 363 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [74 Valid, 289 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:49,564 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1091 states.
[2025-04-28 21:21:50,496 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1091 to 1047.
[2025-04-28 21:21:50,505 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1047 states, 91 states have (on average 10.054945054945055) internal successors, (915), 780 states have internal predecessors, (915), 954 states have call successors, (954), 45 states have call predecessors, (954), 45 states have return successors, (9780), 222 states have call predecessors, (9780), 954 states have call successors, (9780)
[2025-04-28 21:21:50,642 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1047 states to 1047 states and 11649 transitions.
[2025-04-28 21:21:50,642 INFO  L79                 Accepts]: Start accepts. Automaton has 1047 states and 11649 transitions. Word has length 19
[2025-04-28 21:21:50,642 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,643 INFO  L485      AbstractCegarLoop]: Abstraction has 1047 states and 11649 transitions.
[2025-04-28 21:21:50,643 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:50,643 INFO  L278                IsEmpty]: Start isEmpty. Operand 1047 states and 11649 transitions.
[2025-04-28 21:21:50,694 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:50,694 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,694 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,694 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:50,695 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,695 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,695 INFO  L85        PathProgramCache]: Analyzing trace with hash -1588834156, now seen corresponding path program 1 times
[2025-04-28 21:21:50,696 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,696 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1380978852]
[2025-04-28 21:21:50,696 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,696 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,702 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:50,706 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:50,706 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,706 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,758 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:50,758 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,759 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1380978852]
[2025-04-28 21:21:50,759 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1380978852] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,759 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,759 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,759 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1737986799]
[2025-04-28 21:21:50,759 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,759 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,760 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,760 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,760 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,760 INFO  L87              Difference]: Start difference. First operand 1047 states and 11649 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:51,877 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,877 INFO  L93              Difference]: Finished difference Result 1283 states and 20343 transitions.
[2025-04-28 21:21:51,878 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:51,878 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-04-28 21:21:51,878 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,355 INFO  L225             Difference]: With dead ends: 1283
[2025-04-28 21:21:52,355 INFO  L226             Difference]: Without dead ends: 1283
[2025-04-28 21:21:52,355 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:52,355 INFO  L437           NwaCegarLoop]: 165 mSDtfsCounter, 31 mSDsluCounter, 150 mSDsCounter, 0 mSdLazyCounter, 423 mSolverCounterSat, 96 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 79 SdHoareTripleChecker+Valid, 315 SdHoareTripleChecker+Invalid, 519 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 96 IncrementalHoareTripleChecker+Valid, 423 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,356 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [79 Valid, 315 Invalid, 519 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [96 Valid, 423 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:52,357 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1283 states.
[2025-04-28 21:21:53,850 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1283 to 1227.
[2025-04-28 21:21:53,856 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1227 states, 107 states have (on average 9.822429906542055) internal successors, (1051), 912 states have internal predecessors, (1051), 1118 states have call successors, (1118), 53 states have call predecessors, (1118), 53 states have return successors, (12300), 262 states have call predecessors, (12300), 1118 states have call successors, (12300)
[2025-04-28 21:21:54,013 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1227 states to 1227 states and 14469 transitions.
[2025-04-28 21:21:54,013 INFO  L79                 Accepts]: Start accepts. Automaton has 1227 states and 14469 transitions. Word has length 21
[2025-04-28 21:21:54,014 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,014 INFO  L485      AbstractCegarLoop]: Abstraction has 1227 states and 14469 transitions.
[2025-04-28 21:21:54,014 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:54,014 INFO  L278                IsEmpty]: Start isEmpty. Operand 1227 states and 14469 transitions.
[2025-04-28 21:21:54,063 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-04-28 21:21:54,063 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,063 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,063 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:54,064 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,064 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,065 INFO  L85        PathProgramCache]: Analyzing trace with hash -1554670890, now seen corresponding path program 1 times
[2025-04-28 21:21:54,065 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,065 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [980330509]
[2025-04-28 21:21:54,065 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,065 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,072 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-04-28 21:21:54,076 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-04-28 21:21:54,078 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,078 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,125 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:54,125 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,125 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [980330509]
[2025-04-28 21:21:54,125 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [980330509] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,125 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,125 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:54,125 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1024383880]
[2025-04-28 21:21:54,125 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,125 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:54,126 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,126 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:54,126 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:54,126 INFO  L87              Difference]: Start difference. First operand 1227 states and 14469 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
