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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:42,226 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:42,307 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dafaed55-bc6f-4a2f-9a51-d68f5b779806/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:42,312 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:42,313 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:42,337 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:42,338 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:42,338 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:42,338 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:42,338 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:42,339 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:42,339 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:42,339 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:42,339 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:42,339 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:42,339 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:42,339 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:42,339 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:42,339 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:42,340 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:42,340 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:42,340 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:42,340 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:42,340 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:42,340 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:42,341 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:42,341 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:42,651 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:42,660 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:42,664 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:42,665 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:42,666 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:42,669 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dafaed55-bc6f-4a2f-9a51-d68f5b779806/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-232.smt2
[2025-04-28 21:21:42,670 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:42,675 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:43,204 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dafaed55-bc6f-4a2f-9a51-d68f5b779806/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-232.smt2
[2025-04-28 21:21:43,210 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:43,213 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:43,214 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:43,214 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:43,214 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:43,216 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,263 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43 Unit
[2025-04-28 21:21:43,263 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:43,264 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:43,264 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:43,264 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:43,286 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,286 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,322 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,323 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,335 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,341 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,349 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,355 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,357 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,376 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:43,379 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:43,379 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:43,379 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:43,381 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (1/1) ...
[2025-04-28 21:21:43,383 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:43,399 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,412 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:43,416 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:43,427 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:43,427 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:43,428 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:43,428 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Inv given in one single declaration
[2025-04-28 21:21:43,428 INFO  L130     BoogieDeclarations]: Found specification of procedure Inv
[2025-04-28 21:21:43,428 INFO  L138     BoogieDeclarations]: Found implementation of procedure Inv
[2025-04-28 21:21:43,428 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:43,428 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:43,428 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:43,500 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:43,501 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:44,169 INFO  L?                        ?]: Removed 27 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:44,169 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:44,189 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:44,193 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:44,193 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:44 BoogieIcfgContainer
[2025-04-28 21:21:44,193 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:44,195 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:44,197 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:44,201 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:44,201 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:43" (1/3) ...
[2025-04-28 21:21:44,202 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5c3282d9 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:44, skipping insertion in model container
[2025-04-28 21:21:44,202 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:43" (2/3) ...
[2025-04-28 21:21:44,204 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5c3282d9 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:44, skipping insertion in model container
[2025-04-28 21:21:44,204 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:44" (3/3) ...
[2025-04-28 21:21:44,206 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:44,225 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:44,228 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 93 locations, 328 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:44,275 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:44,288 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;@4a31f80d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:44,288 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:44,293 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 93 states, 6 states have (on average 12.166666666666666) internal successors, (73), 73 states have internal predecessors, (73), 84 states have call successors, (85), 2 states have call predecessors, (85), 2 states have return successors, (85), 19 states have call predecessors, (85), 84 states have call successors, (85)
[2025-04-28 21:21:44,358 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-04-28 21:21:44,358 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,359 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-04-28 21:21:44,359 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,364 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,366 INFO  L85        PathProgramCache]: Analyzing trace with hash 529126116, now seen corresponding path program 1 times
[2025-04-28 21:21:44,374 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,374 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [439121233]
[2025-04-28 21:21:44,374 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,375 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,397 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-04-28 21:21:44,399 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-04-28 21:21:44,399 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,400 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,430 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:44,431 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,431 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [439121233]
[2025-04-28 21:21:44,432 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [439121233] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,432 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,436 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-04-28 21:21:44,438 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1476486084]
[2025-04-28 21:21:44,439 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,445 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-04-28 21:21:44,447 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,479 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-04-28 21:21:44,479 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:44,482 INFO  L87              Difference]: Start difference. First operand  has 93 states, 6 states have (on average 12.166666666666666) internal successors, (73), 73 states have internal predecessors, (73), 84 states have call successors, (85), 2 states have call predecessors, (85), 2 states have return successors, (85), 19 states have call predecessors, (85), 84 states have call successors, (85) 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:44,543 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,543 INFO  L93              Difference]: Finished difference Result 91 states and 240 transitions.
[2025-04-28 21:21:44,544 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-04-28 21:21:44,545 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:44,546 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,563 INFO  L225             Difference]: With dead ends: 91
[2025-04-28 21:21:44,563 INFO  L226             Difference]: Without dead ends: 91
[2025-04-28 21:21:44,565 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:44,568 INFO  L437           NwaCegarLoop]: 240 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, 240 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:44,569 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 240 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:44,586 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 91 states.
[2025-04-28 21:21:44,655 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 91 to 91.
[2025-04-28 21:21:44,656 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 91 states, 5 states have (on average 14.0) internal successors, (70), 70 states have internal predecessors, (70), 84 states have call successors, (85), 2 states have call predecessors, (85), 2 states have return successors, (85), 19 states have call predecessors, (85), 84 states have call successors, (85)
[2025-04-28 21:21:44,672 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 91 states to 91 states and 240 transitions.
[2025-04-28 21:21:44,673 INFO  L79                 Accepts]: Start accepts. Automaton has 91 states and 240 transitions. Word has length 5
[2025-04-28 21:21:44,673 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,673 INFO  L485      AbstractCegarLoop]: Abstraction has 91 states and 240 transitions.
[2025-04-28 21:21:44,674 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:44,674 INFO  L278                IsEmpty]: Start isEmpty. Operand 91 states and 240 transitions.
[2025-04-28 21:21:44,703 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:44,703 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,703 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,703 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:44,703 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,704 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,704 INFO  L85        PathProgramCache]: Analyzing trace with hash 1082057947, now seen corresponding path program 1 times
[2025-04-28 21:21:44,704 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,704 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2027917504]
[2025-04-28 21:21:44,705 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,705 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,714 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:44,774 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:44,774 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,774 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,937 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:44,938 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,938 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2027917504]
[2025-04-28 21:21:44,938 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2027917504] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,938 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,938 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:44,942 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1955698794]
[2025-04-28 21:21:44,942 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,944 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:44,948 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,949 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:44,949 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:44,949 INFO  L87              Difference]: Start difference. First operand 91 states and 240 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:46,722 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,722 INFO  L93              Difference]: Finished difference Result 165 states and 530 transitions.
[2025-04-28 21:21:46,723 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:46,723 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:46,723 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,750 INFO  L225             Difference]: With dead ends: 165
[2025-04-28 21:21:46,751 INFO  L226             Difference]: Without dead ends: 165
[2025-04-28 21:21:46,751 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,752 INFO  L437           NwaCegarLoop]: 269 mSDtfsCounter, 56 mSDsluCounter, 325 mSDsCounter, 0 mSdLazyCounter, 471 mSolverCounterSat, 150 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 74 SdHoareTripleChecker+Valid, 594 SdHoareTripleChecker+Invalid, 621 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 150 IncrementalHoareTripleChecker+Valid, 471 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,754 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [74 Valid, 594 Invalid, 621 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [150 Valid, 471 Invalid, 0 Unknown, 0 Unchecked, 1.7s Time]
[2025-04-28 21:21:46,755 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 165 states.
[2025-04-28 21:21:46,876 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 165 to 165.
[2025-04-28 21:21:46,877 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 165 states, 7 states have (on average 18.142857142857142) internal successors, (127), 126 states have internal predecessors, (127), 156 states have call successors, (158), 3 states have call predecessors, (158), 3 states have return successors, (245), 36 states have call predecessors, (245), 156 states have call successors, (245)
[2025-04-28 21:21:46,894 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 165 states to 165 states and 530 transitions.
[2025-04-28 21:21:46,894 INFO  L79                 Accepts]: Start accepts. Automaton has 165 states and 530 transitions. Word has length 9
[2025-04-28 21:21:46,895 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,895 INFO  L485      AbstractCegarLoop]: Abstraction has 165 states and 530 transitions.
[2025-04-28 21:21:46,895 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:46,895 INFO  L278                IsEmpty]: Start isEmpty. Operand 165 states and 530 transitions.
[2025-04-28 21:21:46,963 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:46,964 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,964 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,964 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:46,964 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,965 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,965 INFO  L85        PathProgramCache]: Analyzing trace with hash -1197586891, now seen corresponding path program 1 times
[2025-04-28 21:21:46,965 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,965 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [713887618]
[2025-04-28 21:21:46,965 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,965 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,975 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:46,993 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:46,993 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,993 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,110 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:47,110 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,110 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [713887618]
[2025-04-28 21:21:47,110 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [713887618] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,111 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,111 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:47,111 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1554357094]
[2025-04-28 21:21:47,111 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,111 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:47,111 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,112 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:47,112 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:47,113 INFO  L87              Difference]: Start difference. First operand 165 states and 530 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, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:48,489 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,489 INFO  L93              Difference]: Finished difference Result 239 states and 897 transitions.
[2025-04-28 21:21:48,490 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:48,490 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, (3), 1 states have call predecessors, (3), 2 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:48,490 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,522 INFO  L225             Difference]: With dead ends: 239
[2025-04-28 21:21:48,522 INFO  L226             Difference]: Without dead ends: 239
[2025-04-28 21:21:48,522 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 3 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:48,523 INFO  L437           NwaCegarLoop]: 269 mSDtfsCounter, 56 mSDsluCounter, 326 mSDsCounter, 0 mSdLazyCounter, 466 mSolverCounterSat, 150 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 77 SdHoareTripleChecker+Valid, 595 SdHoareTripleChecker+Invalid, 616 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 150 IncrementalHoareTripleChecker+Valid, 466 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,523 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [77 Valid, 595 Invalid, 616 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [150 Valid, 466 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:48,525 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 239 states.
[2025-04-28 21:21:48,606 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 239 to 165.
[2025-04-28 21:21:48,607 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 165 states, 7 states have (on average 18.142857142857142) internal successors, (127), 126 states have internal predecessors, (127), 156 states have call successors, (158), 3 states have call predecessors, (158), 3 states have return successors, (245), 36 states have call predecessors, (245), 156 states have call successors, (245)
[2025-04-28 21:21:48,615 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 165 states to 165 states and 530 transitions.
[2025-04-28 21:21:48,615 INFO  L79                 Accepts]: Start accepts. Automaton has 165 states and 530 transitions. Word has length 12
[2025-04-28 21:21:48,616 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,616 INFO  L485      AbstractCegarLoop]: Abstraction has 165 states and 530 transitions.
[2025-04-28 21:21:48,616 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, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:48,616 INFO  L278                IsEmpty]: Start isEmpty. Operand 165 states and 530 transitions.
[2025-04-28 21:21:48,671 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:48,672 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,672 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:48,672 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:48,672 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,674 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,674 INFO  L85        PathProgramCache]: Analyzing trace with hash -1301304297, now seen corresponding path program 1 times
[2025-04-28 21:21:48,674 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,674 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [830932858]
[2025-04-28 21:21:48,674 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,674 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,680 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:48,685 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:48,685 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,685 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,727 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:48,727 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,727 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [830932858]
[2025-04-28 21:21:48,728 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [830932858] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,728 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,728 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:48,728 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1003788648]
[2025-04-28 21:21:48,728 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,728 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:48,728 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,729 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:48,729 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:48,729 INFO  L87              Difference]: Start difference. First operand 165 states and 530 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:49,950 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,950 INFO  L93              Difference]: Finished difference Result 313 states and 1271 transitions.
[2025-04-28 21:21:49,951 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:49,952 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:49,952 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,997 INFO  L225             Difference]: With dead ends: 313
[2025-04-28 21:21:49,997 INFO  L226             Difference]: Without dead ends: 313
[2025-04-28 21:21:49,997 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,998 INFO  L437           NwaCegarLoop]: 372 mSDtfsCounter, 56 mSDsluCounter, 439 mSDsCounter, 0 mSdLazyCounter, 479 mSolverCounterSat, 150 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 69 SdHoareTripleChecker+Valid, 811 SdHoareTripleChecker+Invalid, 629 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 150 IncrementalHoareTripleChecker+Valid, 479 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,999 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [69 Valid, 811 Invalid, 629 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [150 Valid, 479 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:21:50,000 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 313 states.
[2025-04-28 21:21:50,152 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 313 to 313.
[2025-04-28 21:21:50,155 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 313 states, 11 states have (on average 21.818181818181817) internal successors, (240), 238 states have internal predecessors, (240), 300 states have call successors, (304), 5 states have call predecessors, (304), 5 states have return successors, (727), 70 states have call predecessors, (727), 300 states have call successors, (727)
[2025-04-28 21:21:50,175 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 313 states to 313 states and 1271 transitions.
[2025-04-28 21:21:50,175 INFO  L79                 Accepts]: Start accepts. Automaton has 313 states and 1271 transitions. Word has length 13
[2025-04-28 21:21:50,175 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,175 INFO  L485      AbstractCegarLoop]: Abstraction has 313 states and 1271 transitions.
[2025-04-28 21:21:50,175 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:50,176 INFO  L278                IsEmpty]: Start isEmpty. Operand 313 states and 1271 transitions.
[2025-04-28 21:21:50,235 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:50,235 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,236 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,236 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:50,236 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,238 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,238 INFO  L85        PathProgramCache]: Analyzing trace with hash -1218082398, now seen corresponding path program 1 times
[2025-04-28 21:21:50,238 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,238 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1650288008]
[2025-04-28 21:21:50,238 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,239 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,246 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:50,258 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:50,258 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,258 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,327 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:50,327 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,327 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1650288008]
[2025-04-28 21:21:50,327 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1650288008] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,327 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,327 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,327 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1486245748]
[2025-04-28 21:21:50,328 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,328 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,328 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,328 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,329 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,329 INFO  L87              Difference]: Start difference. First operand 313 states and 1271 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:52,449 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,449 INFO  L93              Difference]: Finished difference Result 473 states and 3700 transitions.
[2025-04-28 21:21:52,450 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:52,450 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:52,450 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,647 INFO  L225             Difference]: With dead ends: 473
[2025-04-28 21:21:52,647 INFO  L226             Difference]: Without dead ends: 473
[2025-04-28 21:21:52,647 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:52,648 INFO  L437           NwaCegarLoop]: 281 mSDtfsCounter, 57 mSDsluCounter, 295 mSDsCounter, 0 mSdLazyCounter, 725 mSolverCounterSat, 175 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 135 SdHoareTripleChecker+Valid, 576 SdHoareTripleChecker+Invalid, 900 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 175 IncrementalHoareTripleChecker+Valid, 725 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,648 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [135 Valid, 576 Invalid, 900 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [175 Valid, 725 Invalid, 0 Unknown, 0 Unchecked, 2.0s Time]
[2025-04-28 21:21:52,649 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 473 states.
[2025-04-28 21:21:53,114 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 473 to 461.
[2025-04-28 21:21:53,117 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 461 states, 15 states have (on average 23.533333333333335) internal successors, (353), 350 states have internal predecessors, (353), 444 states have call successors, (450), 7 states have call predecessors, (450), 7 states have return successors, (1446), 104 states have call predecessors, (1446), 444 states have call successors, (1446)
[2025-04-28 21:21:53,151 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 461 states to 461 states and 2249 transitions.
[2025-04-28 21:21:53,151 INFO  L79                 Accepts]: Start accepts. Automaton has 461 states and 2249 transitions. Word has length 13
[2025-04-28 21:21:53,151 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,151 INFO  L485      AbstractCegarLoop]: Abstraction has 461 states and 2249 transitions.
[2025-04-28 21:21:53,151 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:53,151 INFO  L278                IsEmpty]: Start isEmpty. Operand 461 states and 2249 transitions.
[2025-04-28 21:21:53,205 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:53,205 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,205 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,205 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:53,206 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,207 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,207 INFO  L85        PathProgramCache]: Analyzing trace with hash -1463333251, now seen corresponding path program 1 times
[2025-04-28 21:21:53,207 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,208 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1034204065]
[2025-04-28 21:21:53,208 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,208 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,214 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:53,228 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:53,228 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,228 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,308 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:53,308 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,309 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1034204065]
[2025-04-28 21:21:53,309 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1034204065] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,309 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,309 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:53,309 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1469338989]
[2025-04-28 21:21:53,309 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,309 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:53,309 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,310 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:53,310 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:53,310 INFO  L87              Difference]: Start difference. First operand 461 states and 2249 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:54,740 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,741 INFO  L93              Difference]: Finished difference Result 683 states and 4092 transitions.
[2025-04-28 21:21:54,741 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:54,741 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:54,742 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,906 INFO  L225             Difference]: With dead ends: 683
[2025-04-28 21:21:54,906 INFO  L226             Difference]: Without dead ends: 683
[2025-04-28 21:21:54,907 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:54,907 INFO  L437           NwaCegarLoop]: 371 mSDtfsCounter, 56 mSDsluCounter, 429 mSDsCounter, 0 mSdLazyCounter, 483 mSolverCounterSat, 150 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 73 SdHoareTripleChecker+Valid, 800 SdHoareTripleChecker+Invalid, 633 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 150 IncrementalHoareTripleChecker+Valid, 483 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,909 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [73 Valid, 800 Invalid, 633 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [150 Valid, 483 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:54,910 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 683 states.
[2025-04-28 21:21:55,632 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 683 to 683.
[2025-04-28 21:21:55,637 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 683 states, 21 states have (on average 25.047619047619047) internal successors, (526), 518 states have internal predecessors, (526), 660 states have call successors, (669), 10 states have call predecessors, (669), 10 states have return successors, (2897), 155 states have call predecessors, (2897), 660 states have call successors, (2897)
[2025-04-28 21:21:55,703 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 683 states to 683 states and 4092 transitions.
[2025-04-28 21:21:55,704 INFO  L79                 Accepts]: Start accepts. Automaton has 683 states and 4092 transitions. Word has length 13
[2025-04-28 21:21:55,704 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,704 INFO  L485      AbstractCegarLoop]: Abstraction has 683 states and 4092 transitions.
[2025-04-28 21:21:55,704 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:55,704 INFO  L278                IsEmpty]: Start isEmpty. Operand 683 states and 4092 transitions.
[2025-04-28 21:21:55,803 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:55,804 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,804 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,804 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:55,804 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,806 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,809 INFO  L85        PathProgramCache]: Analyzing trace with hash 2095881486, now seen corresponding path program 1 times
[2025-04-28 21:21:55,809 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,809 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [193791398]
[2025-04-28 21:21:55,809 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,809 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,818 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:55,823 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:55,825 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,825 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,872 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:55,873 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,873 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [193791398]
[2025-04-28 21:21:55,873 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [193791398] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,873 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,873 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:55,873 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [431034226]
[2025-04-28 21:21:55,873 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,873 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:55,873 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,874 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:55,874 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:55,874 INFO  L87              Difference]: Start difference. First operand 683 states and 4092 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:57,353 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,353 INFO  L93              Difference]: Finished difference Result 905 states and 6424 transitions.
[2025-04-28 21:21:57,354 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:57,354 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:57,354 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,836 INFO  L225             Difference]: With dead ends: 905
[2025-04-28 21:21:57,837 INFO  L226             Difference]: Without dead ends: 905
[2025-04-28 21:21:57,837 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:57,838 INFO  L437           NwaCegarLoop]: 370 mSDtfsCounter, 56 mSDsluCounter, 422 mSDsCounter, 0 mSdLazyCounter, 482 mSolverCounterSat, 150 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 77 SdHoareTripleChecker+Valid, 792 SdHoareTripleChecker+Invalid, 632 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 150 IncrementalHoareTripleChecker+Valid, 482 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,838 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [77 Valid, 792 Invalid, 632 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [150 Valid, 482 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-04-28 21:21:57,839 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 905 states.
[2025-04-28 21:21:58,899 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 905 to 905.
[2025-04-28 21:21:58,906 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 905 states, 27 states have (on average 26.0) internal successors, (702), 686 states have internal predecessors, (702), 876 states have call successors, (888), 13 states have call predecessors, (888), 13 states have return successors, (4834), 206 states have call predecessors, (4834), 876 states have call successors, (4834)
[2025-04-28 21:21:59,018 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 905 states to 905 states and 6424 transitions.
[2025-04-28 21:21:59,018 INFO  L79                 Accepts]: Start accepts. Automaton has 905 states and 6424 transitions. Word has length 13
[2025-04-28 21:21:59,018 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,018 INFO  L485      AbstractCegarLoop]: Abstraction has 905 states and 6424 transitions.
[2025-04-28 21:21:59,019 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:59,019 INFO  L278                IsEmpty]: Start isEmpty. Operand 905 states and 6424 transitions.
[2025-04-28 21:21:59,137 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:59,137 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,137 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,137 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:59,137 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,138 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,138 INFO  L85        PathProgramCache]: Analyzing trace with hash 1360128927, now seen corresponding path program 1 times
[2025-04-28 21:21:59,139 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,139 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [844251051]
[2025-04-28 21:21:59,139 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,139 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,144 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:59,147 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:59,147 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:59,148 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,185 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:59,185 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,185 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [844251051]
[2025-04-28 21:21:59,185 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [844251051] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,185 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:59,185 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:59,185 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [971257668]
[2025-04-28 21:21:59,185 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,186 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:59,186 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,186 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:59,186 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:59,187 INFO  L87              Difference]: Start difference. First operand 905 states and 6424 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:22:00,533 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:00,534 INFO  L93              Difference]: Finished difference Result 1127 states and 9243 transitions.
[2025-04-28 21:22:00,534 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:22:00,535 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:22:00,535 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,070 INFO  L225             Difference]: With dead ends: 1127
[2025-04-28 21:22:01,070 INFO  L226             Difference]: Without dead ends: 1127
[2025-04-28 21:22:01,070 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:22:01,071 INFO  L437           NwaCegarLoop]: 371 mSDtfsCounter, 56 mSDsluCounter, 422 mSDsCounter, 0 mSdLazyCounter, 473 mSolverCounterSat, 150 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 83 SdHoareTripleChecker+Valid, 793 SdHoareTripleChecker+Invalid, 623 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 150 IncrementalHoareTripleChecker+Valid, 473 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,071 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [83 Valid, 793 Invalid, 623 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [150 Valid, 473 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:22:01,073 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1127 states.
[2025-04-28 21:22:02,556 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1127 to 1127.
[2025-04-28 21:22:02,565 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1127 states, 33 states have (on average 26.636363636363637) internal successors, (879), 854 states have internal predecessors, (879), 1092 states have call successors, (1107), 16 states have call predecessors, (1107), 16 states have return successors, (7257), 257 states have call predecessors, (7257), 1092 states have call successors, (7257)
[2025-04-28 21:22:02,826 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1127 states to 1127 states and 9243 transitions.
[2025-04-28 21:22:02,827 INFO  L79                 Accepts]: Start accepts. Automaton has 1127 states and 9243 transitions. Word has length 13
[2025-04-28 21:22:02,827 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:02,827 INFO  L485      AbstractCegarLoop]: Abstraction has 1127 states and 9243 transitions.
[2025-04-28 21:22:02,827 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:22:02,827 INFO  L278                IsEmpty]: Start isEmpty. Operand 1127 states and 9243 transitions.
[2025-04-28 21:22:02,983 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:22:02,983 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:02,983 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:02,983 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:22:02,984 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,986 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,986 INFO  L85        PathProgramCache]: Analyzing trace with hash -1148123542, now seen corresponding path program 1 times
[2025-04-28 21:22:02,986 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,986 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2108984502]
[2025-04-28 21:22:02,986 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:02,986 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,992 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:22:03,001 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:22:03,002 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:03,002 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:03,055 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:03,055 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:03,056 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2108984502]
[2025-04-28 21:22:03,056 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2108984502] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:03,056 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:03,056 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:03,056 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [167340356]
[2025-04-28 21:22:03,056 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,056 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:03,057 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,057 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:03,057 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:03,057 INFO  L87              Difference]: Start difference. First operand 1127 states and 9243 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), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:22:05,394 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:05,395 INFO  L93              Difference]: Finished difference Result 1157 states and 16504 transitions.
[2025-04-28 21:22:05,395 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:05,395 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), 2 states have call predecessors, (4), 2 states have call successors, (4) Word has length 16
[2025-04-28 21:22:05,395 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,242 INFO  L225             Difference]: With dead ends: 1157
[2025-04-28 21:22:06,242 INFO  L226             Difference]: Without dead ends: 1157
[2025-04-28 21:22:06,243 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:22:06,243 INFO  L437           NwaCegarLoop]: 291 mSDtfsCounter, 57 mSDsluCounter, 307 mSDsCounter, 0 mSdLazyCounter, 687 mSolverCounterSat, 175 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 138 SdHoareTripleChecker+Valid, 598 SdHoareTripleChecker+Invalid, 862 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 175 IncrementalHoareTripleChecker+Valid, 687 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,243 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [138 Valid, 598 Invalid, 862 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [175 Valid, 687 Invalid, 0 Unknown, 0 Unchecked, 1.9s Time]
[2025-04-28 21:22:06,245 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1157 states.
[2025-04-28 21:22:08,051 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1157 to 757.
[2025-04-28 21:22:08,057 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 757 states, 23 states have (on average 26.0) internal successors, (598), 574 states have internal predecessors, (598), 732 states have call successors, (742), 11 states have call predecessors, (742), 11 states have return successors, (3602), 172 states have call predecessors, (3602), 732 states have call successors, (3602)
[2025-04-28 21:22:08,143 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 757 states to 757 states and 4942 transitions.
[2025-04-28 21:22:08,144 INFO  L79                 Accepts]: Start accepts. Automaton has 757 states and 4942 transitions. Word has length 16
[2025-04-28 21:22:08,144 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,144 INFO  L485      AbstractCegarLoop]: Abstraction has 757 states and 4942 transitions.
[2025-04-28 21:22:08,144 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), 2 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:22:08,144 INFO  L278                IsEmpty]: Start isEmpty. Operand 757 states and 4942 transitions.
[2025-04-28 21:22:08,262 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:22:08,262 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,262 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:08,262 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:22:08,262 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:08,264 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:08,265 INFO  L85        PathProgramCache]: Analyzing trace with hash 232170865, now seen corresponding path program 1 times
[2025-04-28 21:22:08,265 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:08,266 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2127003922]
[2025-04-28 21:22:08,266 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:08,267 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:08,274 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:22:08,280 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:22:08,280 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:08,280 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:08,328 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:08,328 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:08,328 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2127003922]
[2025-04-28 21:22:08,329 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2127003922] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:08,329 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:08,329 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:08,329 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [180486781]
[2025-04-28 21:22:08,329 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,329 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:08,329 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,330 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:08,330 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:08,331 INFO  L87              Difference]: Start difference. First operand 757 states and 4942 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:22:10,443 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:10,443 INFO  L93              Difference]: Finished difference Result 1157 states and 16484 transitions.
[2025-04-28 21:22:10,444 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:22:10,444 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 16
[2025-04-28 21:22:10,444 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:11,192 INFO  L225             Difference]: With dead ends: 1157
[2025-04-28 21:22:11,192 INFO  L226             Difference]: Without dead ends: 1157
[2025-04-28 21:22:11,193 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:22:11,193 INFO  L437           NwaCegarLoop]: 283 mSDtfsCounter, 57 mSDsluCounter, 301 mSDsCounter, 0 mSdLazyCounter, 652 mSolverCounterSat, 188 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 147 SdHoareTripleChecker+Valid, 584 SdHoareTripleChecker+Invalid, 840 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 188 IncrementalHoareTripleChecker+Valid, 652 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:11,193 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [147 Valid, 584 Invalid, 840 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [188 Valid, 652 Invalid, 0 Unknown, 0 Unchecked, 1.8s Time]
[2025-04-28 21:22:11,195 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1157 states.
[2025-04-28 21:22:12,971 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1157 to 1127.
[2025-04-28 21:22:12,979 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1127 states, 33 states have (on average 26.636363636363637) internal successors, (879), 854 states have internal predecessors, (879), 1092 states have call successors, (1107), 16 states have call predecessors, (1107), 16 states have return successors, (7242), 257 states have call predecessors, (7242), 1092 states have call successors, (7242)
[2025-04-28 21:22:13,159 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1127 states to 1127 states and 9228 transitions.
[2025-04-28 21:22:13,160 INFO  L79                 Accepts]: Start accepts. Automaton has 1127 states and 9228 transitions. Word has length 16
[2025-04-28 21:22:13,160 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:13,160 INFO  L485      AbstractCegarLoop]: Abstraction has 1127 states and 9228 transitions.
[2025-04-28 21:22:13,160 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:22:13,160 INFO  L278                IsEmpty]: Start isEmpty. Operand 1127 states and 9228 transitions.
[2025-04-28 21:22:13,328 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:22:13,328 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:13,328 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:13,328 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:22:13,328 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,330 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,330 INFO  L85        PathProgramCache]: Analyzing trace with hash 589663812, now seen corresponding path program 1 times
[2025-04-28 21:22:13,330 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,330 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1531301078]
[2025-04-28 21:22:13,330 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:13,330 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,336 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:22:13,339 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:22:13,339 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,339 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,386 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:22:13,386 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,386 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1531301078]
[2025-04-28 21:22:13,386 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1531301078] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:13,386 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:13,386 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:22:13,387 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2056147382]
[2025-04-28 21:22:13,387 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:13,387 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:22:13,387 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:13,387 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:22:13,387 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:22:13,387 INFO  L87              Difference]: Start difference. First operand 1127 states and 9228 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)
