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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:28,288 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:28,388 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_621096c7-36c4-4543-adda-70a3f5d4ac9a/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:28,395 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:28,395 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:28,431 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:28,432 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:28,432 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:28,434 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:28,434 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:28,435 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:28,435 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:28,435 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:28,435 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:28,436 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:28,436 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:28,437 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:28,437 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:28,438 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:28,438 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:28,438 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:28,438 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:28,438 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:28,438 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:28,438 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:28,439 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:28,439 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:28,793 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:28,805 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:28,807 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:28,810 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:28,811 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:28,813 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_621096c7-36c4-4543-adda-70a3f5d4ac9a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-226.smt2
[2025-04-28 21:21:28,815 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:28,820 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:29,488 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_621096c7-36c4-4543-adda-70a3f5d4ac9a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Arrays/chc-comp24-LIA-Arrays-226.smt2
[2025-04-28 21:21:29,492 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:29,497 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:29,498 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:29,498 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:29,498 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:29,500 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,560 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29 Unit
[2025-04-28 21:21:29,566 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:29,567 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:29,567 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:29,567 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:29,582 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,583 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,630 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,630 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,650 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,660 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,666 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,677 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,679 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,695 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:29,695 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:29,696 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:29,696 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:29,697 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (1/1) ...
[2025-04-28 21:21:29,699 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:29,720 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,734 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:29,739 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:29,755 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:29,756 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:29,756 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:29,756 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Inv given in one single declaration
[2025-04-28 21:21:29,756 INFO  L130     BoogieDeclarations]: Found specification of procedure Inv
[2025-04-28 21:21:29,756 INFO  L138     BoogieDeclarations]: Found implementation of procedure Inv
[2025-04-28 21:21:29,756 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:29,756 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:29,756 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:29,839 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:29,841 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:30,748 INFO  L?                        ?]: Removed 107 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:30,749 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:30,768 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:30,768 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:30,769 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:30 BoogieIcfgContainer
[2025-04-28 21:21:30,769 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:30,774 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:30,774 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:30,779 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:30,779 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:29" (1/3) ...
[2025-04-28 21:21:30,780 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6d10a265 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:30, skipping insertion in model container
[2025-04-28 21:21:30,780 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:29" (2/3) ...
[2025-04-28 21:21:30,780 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@6d10a265 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:30, skipping insertion in model container
[2025-04-28 21:21:30,781 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:30" (3/3) ...
[2025-04-28 21:21:30,783 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:30,798 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:30,800 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 121 locations, 432 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:30,849 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:30,869 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;@7d99abaa, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:30,871 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:30,875 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 121 states, 6 states have (on average 15.5) internal successors, (93), 93 states have internal predecessors, (93), 112 states have call successors, (113), 2 states have call predecessors, (113), 2 states have return successors, (113), 27 states have call predecessors, (113), 112 states have call successors, (113)
[2025-04-28 21:21:30,964 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-04-28 21:21:30,964 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,965 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-04-28 21:21:30,965 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,972 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,973 INFO  L85        PathProgramCache]: Analyzing trace with hash 683909968, now seen corresponding path program 1 times
[2025-04-28 21:21:30,981 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,981 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1048617544]
[2025-04-28 21:21:30,982 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,982 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,005 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-04-28 21:21:31,008 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-04-28 21:21:31,009 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,009 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,044 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:31,044 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,044 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1048617544]
[2025-04-28 21:21:31,045 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1048617544] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:31,045 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:31,050 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-04-28 21:21:31,052 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [502052151]
[2025-04-28 21:21:31,053 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,060 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-04-28 21:21:31,061 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,098 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-04-28 21:21:31,098 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:31,101 INFO  L87              Difference]: Start difference. First operand  has 121 states, 6 states have (on average 15.5) internal successors, (93), 93 states have internal predecessors, (93), 112 states have call successors, (113), 2 states have call predecessors, (113), 2 states have return successors, (113), 27 states have call predecessors, (113), 112 states have call successors, (113) 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:31,171 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,172 INFO  L93              Difference]: Finished difference Result 119 states and 316 transitions.
[2025-04-28 21:21:31,172 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-04-28 21:21:31,175 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:31,175 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,210 INFO  L225             Difference]: With dead ends: 119
[2025-04-28 21:21:31,210 INFO  L226             Difference]: Without dead ends: 119
[2025-04-28 21:21:31,212 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:31,216 INFO  L437           NwaCegarLoop]: 316 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, 316 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:31,220 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 316 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:31,237 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 119 states.
[2025-04-28 21:21:31,382 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 119 to 119.
[2025-04-28 21:21:31,384 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 119 states, 5 states have (on average 18.0) internal successors, (90), 90 states have internal predecessors, (90), 112 states have call successors, (113), 2 states have call predecessors, (113), 2 states have return successors, (113), 27 states have call predecessors, (113), 112 states have call successors, (113)
[2025-04-28 21:21:31,404 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 119 states to 119 states and 316 transitions.
[2025-04-28 21:21:31,408 INFO  L79                 Accepts]: Start accepts. Automaton has 119 states and 316 transitions. Word has length 5
[2025-04-28 21:21:31,408 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,408 INFO  L485      AbstractCegarLoop]: Abstraction has 119 states and 316 transitions.
[2025-04-28 21:21:31,408 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:31,409 INFO  L278                IsEmpty]: Start isEmpty. Operand 119 states and 316 transitions.
[2025-04-28 21:21:31,462 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:31,463 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,463 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,463 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:31,463 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,464 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,464 INFO  L85        PathProgramCache]: Analyzing trace with hash -976983281, now seen corresponding path program 1 times
[2025-04-28 21:21:31,464 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,465 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [431059243]
[2025-04-28 21:21:31,465 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,465 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,472 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:31,505 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:31,505 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,505 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,661 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:31,661 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,661 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [431059243]
[2025-04-28 21:21:31,661 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [431059243] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:31,661 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:31,662 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:31,662 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [615555034]
[2025-04-28 21:21:31,662 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,663 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:31,665 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,665 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:31,666 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:31,666 INFO  L87              Difference]: Start difference. First operand 119 states and 316 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:34,099 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,100 INFO  L93              Difference]: Finished difference Result 217 states and 700 transitions.
[2025-04-28 21:21:34,100 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:34,101 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:34,101 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,136 INFO  L225             Difference]: With dead ends: 217
[2025-04-28 21:21:34,136 INFO  L226             Difference]: Without dead ends: 217
[2025-04-28 21:21:34,137 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:34,138 INFO  L437           NwaCegarLoop]: 349 mSDtfsCounter, 72 mSDsluCounter, 419 mSDsCounter, 0 mSdLazyCounter, 623 mSolverCounterSat, 198 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 99 SdHoareTripleChecker+Valid, 768 SdHoareTripleChecker+Invalid, 821 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 198 IncrementalHoareTripleChecker+Valid, 623 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,138 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [99 Valid, 768 Invalid, 821 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [198 Valid, 623 Invalid, 0 Unknown, 0 Unchecked, 2.3s Time]
[2025-04-28 21:21:34,139 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 217 states.
[2025-04-28 21:21:34,323 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 217 to 217.
[2025-04-28 21:21:34,324 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 217 states, 7 states have (on average 23.285714285714285) internal successors, (163), 162 states have internal predecessors, (163), 208 states have call successors, (210), 3 states have call predecessors, (210), 3 states have return successors, (327), 52 states have call predecessors, (327), 208 states have call successors, (327)
[2025-04-28 21:21:34,341 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 217 states to 217 states and 700 transitions.
[2025-04-28 21:21:34,341 INFO  L79                 Accepts]: Start accepts. Automaton has 217 states and 700 transitions. Word has length 9
[2025-04-28 21:21:34,344 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,344 INFO  L485      AbstractCegarLoop]: Abstraction has 217 states and 700 transitions.
[2025-04-28 21:21:34,344 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:34,344 INFO  L278                IsEmpty]: Start isEmpty. Operand 217 states and 700 transitions.
[2025-04-28 21:21:34,425 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:34,425 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,426 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,426 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:34,426 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,428 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,428 INFO  L85        PathProgramCache]: Analyzing trace with hash 841272431, now seen corresponding path program 1 times
[2025-04-28 21:21:34,428 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,428 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1522020911]
[2025-04-28 21:21:34,428 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,428 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,435 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:34,452 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:34,452 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,452 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,581 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:34,585 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,585 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1522020911]
[2025-04-28 21:21:34,585 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1522020911] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:34,585 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:34,585 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:34,585 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [765400548]
[2025-04-28 21:21:34,585 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,585 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:34,585 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,586 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:34,586 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:34,586 INFO  L87              Difference]: Start difference. First operand 217 states and 700 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:36,304 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,304 INFO  L93              Difference]: Finished difference Result 315 states and 1187 transitions.
[2025-04-28 21:21:36,305 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:36,305 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:36,305 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,366 INFO  L225             Difference]: With dead ends: 315
[2025-04-28 21:21:36,367 INFO  L226             Difference]: Without dead ends: 315
[2025-04-28 21:21:36,367 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:36,368 INFO  L437           NwaCegarLoop]: 349 mSDtfsCounter, 72 mSDsluCounter, 420 mSDsCounter, 0 mSdLazyCounter, 626 mSolverCounterSat, 198 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 98 SdHoareTripleChecker+Valid, 769 SdHoareTripleChecker+Invalid, 824 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 198 IncrementalHoareTripleChecker+Valid, 626 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,368 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [98 Valid, 769 Invalid, 824 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [198 Valid, 626 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:21:36,369 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 315 states.
[2025-04-28 21:21:36,528 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 315 to 217.
[2025-04-28 21:21:36,529 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 217 states, 7 states have (on average 23.285714285714285) internal successors, (163), 162 states have internal predecessors, (163), 208 states have call successors, (210), 3 states have call predecessors, (210), 3 states have return successors, (327), 52 states have call predecessors, (327), 208 states have call successors, (327)
[2025-04-28 21:21:36,541 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 217 states to 217 states and 700 transitions.
[2025-04-28 21:21:36,541 INFO  L79                 Accepts]: Start accepts. Automaton has 217 states and 700 transitions. Word has length 12
[2025-04-28 21:21:36,542 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,542 INFO  L485      AbstractCegarLoop]: Abstraction has 217 states and 700 transitions.
[2025-04-28 21:21:36,542 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:36,543 INFO  L278                IsEmpty]: Start isEmpty. Operand 217 states and 700 transitions.
[2025-04-28 21:21:36,611 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:36,611 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,611 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,611 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:36,611 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,612 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,612 INFO  L85        PathProgramCache]: Analyzing trace with hash 701174839, now seen corresponding path program 1 times
[2025-04-28 21:21:36,612 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,612 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1236691191]
[2025-04-28 21:21:36,612 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,612 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,621 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:36,627 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:36,628 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,628 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,700 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:36,700 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,700 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1236691191]
[2025-04-28 21:21:36,701 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1236691191] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,701 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,701 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:36,701 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1704861044]
[2025-04-28 21:21:36,701 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,701 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:36,701 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,702 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:36,702 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:36,703 INFO  L87              Difference]: Start difference. First operand 217 states and 700 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:39,755 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,755 INFO  L93              Difference]: Finished difference Result 321 states and 1827 transitions.
[2025-04-28 21:21:39,759 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:39,759 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:39,760 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,829 INFO  L225             Difference]: With dead ends: 321
[2025-04-28 21:21:39,829 INFO  L226             Difference]: Without dead ends: 321
[2025-04-28 21:21:39,830 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:39,832 INFO  L437           NwaCegarLoop]: 357 mSDtfsCounter, 73 mSDsluCounter, 380 mSDsCounter, 0 mSdLazyCounter, 953 mSolverCounterSat, 234 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 173 SdHoareTripleChecker+Valid, 737 SdHoareTripleChecker+Invalid, 1187 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 234 IncrementalHoareTripleChecker+Valid, 953 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,833 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [173 Valid, 737 Invalid, 1187 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [234 Valid, 953 Invalid, 0 Unknown, 0 Unchecked, 2.9s Time]
[2025-04-28 21:21:39,833 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 321 states.
[2025-04-28 21:21:40,059 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 321 to 315.
[2025-04-28 21:21:40,061 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 315 states, 9 states have (on average 26.22222222222222) internal successors, (236), 234 states have internal predecessors, (236), 304 states have call successors, (307), 4 states have call predecessors, (307), 4 states have return successors, (641), 77 states have call predecessors, (641), 304 states have call successors, (641)
[2025-04-28 21:21:40,086 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 315 states to 315 states and 1184 transitions.
[2025-04-28 21:21:40,086 INFO  L79                 Accepts]: Start accepts. Automaton has 315 states and 1184 transitions. Word has length 13
[2025-04-28 21:21:40,087 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,087 INFO  L485      AbstractCegarLoop]: Abstraction has 315 states and 1184 transitions.
[2025-04-28 21:21:40,087 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:40,087 INFO  L278                IsEmpty]: Start isEmpty. Operand 315 states and 1184 transitions.
[2025-04-28 21:21:40,185 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:40,185 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,186 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,186 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:40,186 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,186 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,186 INFO  L85        PathProgramCache]: Analyzing trace with hash -334998153, now seen corresponding path program 1 times
[2025-04-28 21:21:40,187 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,187 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1880497195]
[2025-04-28 21:21:40,187 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,187 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,194 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:40,204 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:40,207 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,208 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,255 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:40,255 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,256 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1880497195]
[2025-04-28 21:21:40,256 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1880497195] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,256 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,256 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:40,256 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1112923237]
[2025-04-28 21:21:40,256 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,256 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:40,256 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,257 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:40,257 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:40,257 INFO  L87              Difference]: Start difference. First operand 315 states and 1184 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:41,983 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,983 INFO  L93              Difference]: Finished difference Result 609 states and 2993 transitions.
[2025-04-28 21:21:41,983 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:41,984 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:41,984 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,126 INFO  L225             Difference]: With dead ends: 609
[2025-04-28 21:21:42,126 INFO  L226             Difference]: Without dead ends: 609
[2025-04-28 21:21:42,126 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:42,127 INFO  L437           NwaCegarLoop]: 489 mSDtfsCounter, 72 mSDsluCounter, 560 mSDsCounter, 0 mSdLazyCounter, 645 mSolverCounterSat, 198 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 99 SdHoareTripleChecker+Valid, 1049 SdHoareTripleChecker+Invalid, 843 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 198 IncrementalHoareTripleChecker+Valid, 645 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,128 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [99 Valid, 1049 Invalid, 843 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [198 Valid, 645 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:21:42,131 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 609 states.
[2025-04-28 21:21:42,554 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 609 to 609.
[2025-04-28 21:21:42,558 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 609 states, 15 states have (on average 30.733333333333334) internal successors, (461), 450 states have internal predecessors, (461), 592 states have call successors, (598), 7 states have call predecessors, (598), 7 states have return successors, (1934), 152 states have call predecessors, (1934), 592 states have call successors, (1934)
[2025-04-28 21:21:42,616 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 609 states to 609 states and 2993 transitions.
[2025-04-28 21:21:42,616 INFO  L79                 Accepts]: Start accepts. Automaton has 609 states and 2993 transitions. Word has length 13
[2025-04-28 21:21:42,616 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,617 INFO  L485      AbstractCegarLoop]: Abstraction has 609 states and 2993 transitions.
[2025-04-28 21:21:42,617 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:42,617 INFO  L278                IsEmpty]: Start isEmpty. Operand 609 states and 2993 transitions.
[2025-04-28 21:21:42,717 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:42,717 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,717 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,717 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:42,718 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,719 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,719 INFO  L85        PathProgramCache]: Analyzing trace with hash 2106385806, now seen corresponding path program 1 times
[2025-04-28 21:21:42,719 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,719 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [901938513]
[2025-04-28 21:21:42,719 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,719 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,725 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:42,728 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:42,728 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,728 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,797 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:42,798 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,798 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [901938513]
[2025-04-28 21:21:42,798 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [901938513] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,798 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,798 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:42,798 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1640115073]
[2025-04-28 21:21:42,798 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,798 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:42,798 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,799 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:42,799 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:42,799 INFO  L87              Difference]: Start difference. First operand 609 states and 2993 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:44,638 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,639 INFO  L93              Difference]: Finished difference Result 903 states and 5457 transitions.
[2025-04-28 21:21:44,639 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:44,640 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:44,640 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,957 INFO  L225             Difference]: With dead ends: 903
[2025-04-28 21:21:44,957 INFO  L226             Difference]: Without dead ends: 903
[2025-04-28 21:21:44,957 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:44,958 INFO  L437           NwaCegarLoop]: 484 mSDtfsCounter, 72 mSDsluCounter, 552 mSDsCounter, 0 mSdLazyCounter, 626 mSolverCounterSat, 198 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 110 SdHoareTripleChecker+Valid, 1036 SdHoareTripleChecker+Invalid, 824 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 198 IncrementalHoareTripleChecker+Valid, 626 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,958 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [110 Valid, 1036 Invalid, 824 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [198 Valid, 626 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:21:44,963 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 903 states.
[2025-04-28 21:21:45,938 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 903 to 903.
[2025-04-28 21:21:45,944 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 903 states, 21 states have (on average 32.714285714285715) internal successors, (687), 666 states have internal predecessors, (687), 880 states have call successors, (889), 10 states have call predecessors, (889), 10 states have return successors, (3881), 227 states have call predecessors, (3881), 880 states have call successors, (3881)
[2025-04-28 21:21:46,094 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 903 states to 903 states and 5457 transitions.
[2025-04-28 21:21:46,094 INFO  L79                 Accepts]: Start accepts. Automaton has 903 states and 5457 transitions. Word has length 13
[2025-04-28 21:21:46,094 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,094 INFO  L485      AbstractCegarLoop]: Abstraction has 903 states and 5457 transitions.
[2025-04-28 21:21:46,095 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:46,095 INFO  L278                IsEmpty]: Start isEmpty. Operand 903 states and 5457 transitions.
[2025-04-28 21:21:46,196 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:46,196 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,196 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,196 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:46,196 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,198 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,199 INFO  L85        PathProgramCache]: Analyzing trace with hash 1716487022, now seen corresponding path program 1 times
[2025-04-28 21:21:46,200 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,200 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1705693762]
[2025-04-28 21:21:46,201 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,201 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,208 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:46,212 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:46,216 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,217 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,282 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:46,283 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,283 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1705693762]
[2025-04-28 21:21:46,283 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1705693762] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,283 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,283 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:46,283 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [355769699]
[2025-04-28 21:21:46,283 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,283 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:46,284 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,284 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:46,285 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,285 INFO  L87              Difference]: Start difference. First operand 903 states and 5457 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:48,210 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,211 INFO  L93              Difference]: Finished difference Result 1197 states and 8578 transitions.
[2025-04-28 21:21:48,211 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:48,211 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:48,212 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,713 INFO  L225             Difference]: With dead ends: 1197
[2025-04-28 21:21:48,713 INFO  L226             Difference]: Without dead ends: 1197
[2025-04-28 21:21:48,713 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:48,713 INFO  L437           NwaCegarLoop]: 477 mSDtfsCounter, 72 mSDsluCounter, 539 mSDsCounter, 0 mSdLazyCounter, 631 mSolverCounterSat, 198 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 113 SdHoareTripleChecker+Valid, 1016 SdHoareTripleChecker+Invalid, 829 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 198 IncrementalHoareTripleChecker+Valid, 631 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,714 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [113 Valid, 1016 Invalid, 829 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [198 Valid, 631 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:21:48,715 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1197 states.
[2025-04-28 21:21:50,020 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1197 to 1197.
[2025-04-28 21:21:50,029 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1197 states, 27 states have (on average 33.925925925925924) internal successors, (916), 882 states have internal predecessors, (916), 1168 states have call successors, (1180), 13 states have call predecessors, (1180), 13 states have return successors, (6482), 302 states have call predecessors, (6482), 1168 states have call successors, (6482)
[2025-04-28 21:21:50,237 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1197 states to 1197 states and 8578 transitions.
[2025-04-28 21:21:50,237 INFO  L79                 Accepts]: Start accepts. Automaton has 1197 states and 8578 transitions. Word has length 13
[2025-04-28 21:21:50,237 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,237 INFO  L485      AbstractCegarLoop]: Abstraction has 1197 states and 8578 transitions.
[2025-04-28 21:21:50,237 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,237 INFO  L278                IsEmpty]: Start isEmpty. Operand 1197 states and 8578 transitions.
[2025-04-28 21:21:50,606 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:50,606 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,606 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,606 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:50,606 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,607 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,607 INFO  L85        PathProgramCache]: Analyzing trace with hash 1482908203, now seen corresponding path program 1 times
[2025-04-28 21:21:50,607 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,607 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1421800217]
[2025-04-28 21:21:50,607 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,607 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,616 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:50,622 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:50,622 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,623 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,720 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:21:50,721 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,721 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1421800217]
[2025-04-28 21:21:50,721 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1421800217] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,721 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,721 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,721 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1016666357]
[2025-04-28 21:21:50,721 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,722 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,722 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,723 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,723 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,723 INFO  L87              Difference]: Start difference. First operand 1197 states and 8578 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:21:54,115 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,115 INFO  L93              Difference]: Finished difference Result 1221 states and 15047 transitions.
[2025-04-28 21:21:54,116 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:54,116 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:21:54,116 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,900 INFO  L225             Difference]: With dead ends: 1221
[2025-04-28 21:21:54,901 INFO  L226             Difference]: Without dead ends: 1221
[2025-04-28 21:21:54,901 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:54,901 INFO  L437           NwaCegarLoop]: 369 mSDtfsCounter, 73 mSDsluCounter, 392 mSDsCounter, 0 mSdLazyCounter, 937 mSolverCounterSat, 238 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 176 SdHoareTripleChecker+Valid, 761 SdHoareTripleChecker+Invalid, 1175 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 238 IncrementalHoareTripleChecker+Valid, 937 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,902 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [176 Valid, 761 Invalid, 1175 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [238 Valid, 937 Invalid, 0 Unknown, 0 Unchecked, 2.9s Time]
[2025-04-28 21:21:54,903 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1221 states.
[2025-04-28 21:21:56,829 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1221 to 805.
[2025-04-28 21:21:56,833 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 805 states, 19 states have (on average 33.0) internal successors, (627), 594 states have internal predecessors, (627), 784 states have call successors, (792), 9 states have call predecessors, (792), 9 states have return successors, (3216), 202 states have call predecessors, (3216), 784 states have call successors, (3216)
[2025-04-28 21:21:56,902 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 805 states to 805 states and 4635 transitions.
[2025-04-28 21:21:56,903 INFO  L79                 Accepts]: Start accepts. Automaton has 805 states and 4635 transitions. Word has length 16
[2025-04-28 21:21:56,903 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,903 INFO  L485      AbstractCegarLoop]: Abstraction has 805 states and 4635 transitions.
[2025-04-28 21:21:56,903 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:21:56,903 INFO  L278                IsEmpty]: Start isEmpty. Operand 805 states and 4635 transitions.
[2025-04-28 21:21:57,086 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:57,086 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,086 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,086 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:57,086 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:57,088 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:57,089 INFO  L85        PathProgramCache]: Analyzing trace with hash 767436759, now seen corresponding path program 1 times
[2025-04-28 21:21:57,089 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:57,089 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [574109738]
[2025-04-28 21:21:57,089 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,089 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:57,096 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:57,103 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:57,103 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,103 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,148 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:21:57,149 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,149 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [574109738]
[2025-04-28 21:21:57,149 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [574109738] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:57,150 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:57,150 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:57,150 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [230735243]
[2025-04-28 21:21:57,150 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,151 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:57,151 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,152 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:57,152 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:57,152 INFO  L87              Difference]: Start difference. First operand 805 states and 4635 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)
