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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:29,137 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:29,245 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f9c4acac-1762-4d08-893d-aa5e74646389/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:29,253 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:29,255 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:29,288 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:29,288 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:29,289 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:29,289 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:29,290 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:29,291 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:29,291 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:29,291 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:29,292 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:29,293 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:29,293 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:29,293 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:29,293 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:29,293 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:29,293 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:29,294 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:29,294 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:29,294 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:29,294 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:29,295 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:29,296 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:29,296 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:29,661 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:29,675 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:29,679 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:29,682 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:29,682 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:29,684 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f9c4acac-1762-4d08-893d-aa5e74646389/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-192.smt2
[2025-04-28 21:21:29,685 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:29,693 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:30,528 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f9c4acac-1762-4d08-893d-aa5e74646389/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-192.smt2
[2025-04-28 21:21:30,532 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:30,534 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:30,537 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:30,537 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:30,537 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:30,544 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,627 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30 Unit
[2025-04-28 21:21:30,627 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:30,629 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:30,629 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:30,629 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:30,651 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,651 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,690 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,690 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,714 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,720 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,724 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,728 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,731 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,769 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:30,770 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:30,770 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:30,770 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:30,772 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,775 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:30,793 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,810 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:30,816 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:30,832 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:30,833 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:30,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:30,833 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:30,833 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:30,833 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:30,834 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure step_lturn given in one single declaration
[2025-04-28 21:21:30,834 INFO  L130     BoogieDeclarations]: Found specification of procedure step_lturn
[2025-04-28 21:21:30,834 INFO  L138     BoogieDeclarations]: Found implementation of procedure step_lturn
[2025-04-28 21:21:30,835 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure combined_lturn given in one single declaration
[2025-04-28 21:21:30,835 INFO  L130     BoogieDeclarations]: Found specification of procedure combined_lturn
[2025-04-28 21:21:30,835 INFO  L138     BoogieDeclarations]: Found implementation of procedure combined_lturn
[2025-04-28 21:21:30,835 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure lturn given in one single declaration
[2025-04-28 21:21:30,835 INFO  L130     BoogieDeclarations]: Found specification of procedure lturn
[2025-04-28 21:21:30,835 INFO  L138     BoogieDeclarations]: Found implementation of procedure lturn
[2025-04-28 21:21:30,835 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:30,835 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:30,837 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:30,942 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:30,945 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:32,251 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:32,252 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:32,282 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:32,283 INFO  L312             CfgBuilder]: Removed 33 assume(true) statements.
[2025-04-28 21:21:32,284 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:32 BoogieIcfgContainer
[2025-04-28 21:21:32,284 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:32,287 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:32,288 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:32,293 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:32,293 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:30" (1/3) ...
[2025-04-28 21:21:32,294 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4d79d409 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:32, skipping insertion in model container
[2025-04-28 21:21:32,295 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (2/3) ...
[2025-04-28 21:21:32,295 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@4d79d409 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:32, skipping insertion in model container
[2025-04-28 21:21:32,295 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:32" (3/3) ...
[2025-04-28 21:21:32,298 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:32,318 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:32,321 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 6 procedures, 116 locations, 402 edges, 6 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:32,383 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:32,404 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;@21bd0cb7, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:32,405 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:32,409 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 116 states, 9 states have (on average 1.3333333333333333) internal successors, (12), 10 states have internal predecessors, (12), 102 states have call successors, (130), 5 states have call predecessors, (130), 5 states have return successors, (130), 102 states have call predecessors, (130), 102 states have call successors, (130)
[2025-04-28 21:21:32,436 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:32,436 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,437 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,441 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,447 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,448 INFO  L85        PathProgramCache]: Analyzing trace with hash -1443914277, now seen corresponding path program 1 times
[2025-04-28 21:21:32,456 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,457 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1005173470]
[2025-04-28 21:21:32,459 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,460 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,525 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:32,784 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:32,784 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,784 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,998 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:33,999 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,000 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1005173470]
[2025-04-28 21:21:34,000 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1005173470] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:34,001 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:34,004 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:34,006 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2135023426]
[2025-04-28 21:21:34,008 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,013 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:34,015 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,045 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:34,046 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:34,048 INFO  L87              Difference]: Start difference. First operand  has 116 states, 9 states have (on average 1.3333333333333333) internal successors, (12), 10 states have internal predecessors, (12), 102 states have call successors, (130), 5 states have call predecessors, (130), 5 states have return successors, (130), 102 states have call predecessors, (130), 102 states have call successors, (130) Second operand  has 5 states, 4 states have (on average 1.5) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:36,149 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,151 INFO  L93              Difference]: Finished difference Result 192 states and 621 transitions.
[2025-04-28 21:21:36,152 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:36,154 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 18
[2025-04-28 21:21:36,154 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,184 INFO  L225             Difference]: With dead ends: 192
[2025-04-28 21:21:36,184 INFO  L226             Difference]: Without dead ends: 192
[2025-04-28 21:21:36,186 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:36,189 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 1 mSDsluCounter, 578 mSDsCounter, 0 mSdLazyCounter, 788 mSolverCounterSat, 58 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 117 SdHoareTripleChecker+Valid, 840 SdHoareTripleChecker+Invalid, 846 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 58 IncrementalHoareTripleChecker+Valid, 788 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,190 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [117 Valid, 840 Invalid, 846 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [58 Valid, 788 Invalid, 0 Unknown, 0 Unchecked, 1.9s Time]
[2025-04-28 21:21:36,209 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 192 states.
[2025-04-28 21:21:36,472 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 192 to 180.
[2025-04-28 21:21:36,475 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 180 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 10 states have internal predecessors, (13), 164 states have call successors, (201), 7 states have call predecessors, (201), 7 states have return successors, (375), 164 states have call predecessors, (375), 164 states have call successors, (375)
[2025-04-28 21:21:36,484 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 180 states to 180 states and 589 transitions.
[2025-04-28 21:21:36,485 INFO  L79                 Accepts]: Start accepts. Automaton has 180 states and 589 transitions. Word has length 18
[2025-04-28 21:21:36,486 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,487 INFO  L485      AbstractCegarLoop]: Abstraction has 180 states and 589 transitions.
[2025-04-28 21:21:36,487 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:36,487 INFO  L278                IsEmpty]: Start isEmpty. Operand 180 states and 589 transitions.
[2025-04-28 21:21:36,500 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:36,500 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,500 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,503 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:36,505 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,506 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,506 INFO  L85        PathProgramCache]: Analyzing trace with hash -263007763, now seen corresponding path program 1 times
[2025-04-28 21:21:36,506 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,506 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1646357862]
[2025-04-28 21:21:36,506 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,506 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,537 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:36,608 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:36,608 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,608 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,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:36,938 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,938 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1646357862]
[2025-04-28 21:21:36,939 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1646357862] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,939 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,940 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:36,940 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1820975090]
[2025-04-28 21:21:36,940 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,941 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:36,941 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,942 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:36,942 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:36,942 INFO  L87              Difference]: Start difference. First operand 180 states and 589 transitions. Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:38,535 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,535 INFO  L93              Difference]: Finished difference Result 232 states and 976 transitions.
[2025-04-28 21:21:38,536 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:38,536 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 18
[2025-04-28 21:21:38,536 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,549 INFO  L225             Difference]: With dead ends: 232
[2025-04-28 21:21:38,549 INFO  L226             Difference]: Without dead ends: 232
[2025-04-28 21:21:38,550 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:38,551 INFO  L437           NwaCegarLoop]: 283 mSDtfsCounter, 2 mSDsluCounter, 963 mSDsCounter, 0 mSdLazyCounter, 878 mSolverCounterSat, 42 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 50 SdHoareTripleChecker+Valid, 1246 SdHoareTripleChecker+Invalid, 920 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 42 IncrementalHoareTripleChecker+Valid, 878 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,551 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [50 Valid, 1246 Invalid, 920 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [42 Valid, 878 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-04-28 21:21:38,552 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 232 states.
[2025-04-28 21:21:38,749 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 232 to 229.
[2025-04-28 21:21:38,751 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 229 states, 16 states have (on average 1.1875) internal successors, (19), 15 states have internal predecessors, (19), 205 states have call successors, (251), 9 states have call predecessors, (251), 11 states have return successors, (700), 207 states have call predecessors, (700), 205 states have call successors, (700)
[2025-04-28 21:21:38,760 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 229 states to 229 states and 970 transitions.
[2025-04-28 21:21:38,760 INFO  L79                 Accepts]: Start accepts. Automaton has 229 states and 970 transitions. Word has length 18
[2025-04-28 21:21:38,760 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,761 INFO  L485      AbstractCegarLoop]: Abstraction has 229 states and 970 transitions.
[2025-04-28 21:21:38,762 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:38,762 INFO  L278                IsEmpty]: Start isEmpty. Operand 229 states and 970 transitions.
[2025-04-28 21:21:38,777 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:38,777 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,777 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,777 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:38,778 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,779 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,781 INFO  L85        PathProgramCache]: Analyzing trace with hash 2066731675, now seen corresponding path program 1 times
[2025-04-28 21:21:38,781 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,781 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2107750470]
[2025-04-28 21:21:38,781 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,781 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,809 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:38,861 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:38,861 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,861 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,349 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:39,349 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,349 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2107750470]
[2025-04-28 21:21:39,350 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2107750470] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,350 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,350 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:39,350 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [657669634]
[2025-04-28 21:21:39,350 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,350 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:39,350 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,351 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:39,351 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:39,351 INFO  L87              Difference]: Start difference. First operand 229 states and 970 transitions. Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:41,230 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,231 INFO  L93              Difference]: Finished difference Result 322 states and 1992 transitions.
[2025-04-28 21:21:41,231 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:41,232 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 18
[2025-04-28 21:21:41,232 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,255 INFO  L225             Difference]: With dead ends: 322
[2025-04-28 21:21:41,255 INFO  L226             Difference]: Without dead ends: 322
[2025-04-28 21:21:41,256 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:41,257 INFO  L437           NwaCegarLoop]: 291 mSDtfsCounter, 2 mSDsluCounter, 980 mSDsCounter, 0 mSdLazyCounter, 905 mSolverCounterSat, 30 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 46 SdHoareTripleChecker+Valid, 1271 SdHoareTripleChecker+Invalid, 935 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 30 IncrementalHoareTripleChecker+Valid, 905 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,258 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [46 Valid, 1271 Invalid, 935 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [30 Valid, 905 Invalid, 0 Unknown, 0 Unchecked, 1.8s Time]
[2025-04-28 21:21:41,260 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 322 states.
[2025-04-28 21:21:41,653 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 322 to 318.
[2025-04-28 21:21:41,656 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 318 states, 27 states have (on average 1.1481481481481481) internal successors, (31), 26 states have internal predecessors, (31), 276 states have call successors, (340), 13 states have call predecessors, (340), 20 states have return successors, (1608), 282 states have call predecessors, (1608), 276 states have call successors, (1608)
[2025-04-28 21:21:41,669 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 318 states to 318 states and 1979 transitions.
[2025-04-28 21:21:41,670 INFO  L79                 Accepts]: Start accepts. Automaton has 318 states and 1979 transitions. Word has length 18
[2025-04-28 21:21:41,670 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,670 INFO  L485      AbstractCegarLoop]: Abstraction has 318 states and 1979 transitions.
[2025-04-28 21:21:41,670 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:41,671 INFO  L278                IsEmpty]: Start isEmpty. Operand 318 states and 1979 transitions.
[2025-04-28 21:21:41,682 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:41,682 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,682 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,682 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:41,683 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,683 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,684 INFO  L85        PathProgramCache]: Analyzing trace with hash -1385429165, now seen corresponding path program 1 times
[2025-04-28 21:21:41,684 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,684 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1615845700]
[2025-04-28 21:21:41,684 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,684 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,707 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:41,751 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:41,752 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,752 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,167 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:42,167 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,167 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1615845700]
[2025-04-28 21:21:42,167 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1615845700] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,167 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,168 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:42,168 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [136258455]
[2025-04-28 21:21:42,168 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,168 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:42,168 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,169 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:42,169 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,169 INFO  L87              Difference]: Start difference. First operand 318 states and 1979 transitions. Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:44,301 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,302 INFO  L93              Difference]: Finished difference Result 390 states and 2922 transitions.
[2025-04-28 21:21:44,302 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:44,303 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 18
[2025-04-28 21:21:44,303 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,329 INFO  L225             Difference]: With dead ends: 390
[2025-04-28 21:21:44,329 INFO  L226             Difference]: Without dead ends: 390
[2025-04-28 21:21:44,330 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:44,333 INFO  L437           NwaCegarLoop]: 279 mSDtfsCounter, 2 mSDsluCounter, 952 mSDsCounter, 0 mSdLazyCounter, 855 mSolverCounterSat, 42 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 52 SdHoareTripleChecker+Valid, 1231 SdHoareTripleChecker+Invalid, 897 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 42 IncrementalHoareTripleChecker+Valid, 855 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,334 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [52 Valid, 1231 Invalid, 897 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [42 Valid, 855 Invalid, 0 Unknown, 0 Unchecked, 2.0s Time]
[2025-04-28 21:21:44,336 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 390 states.
[2025-04-28 21:21:44,919 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 390 to 386.
[2025-04-28 21:21:44,924 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 386 states, 35 states have (on average 1.2) internal successors, (42), 33 states have internal predecessors, (42), 332 states have call successors, (414), 17 states have call predecessors, (414), 26 states have return successors, (2451), 340 states have call predecessors, (2451), 332 states have call successors, (2451)
[2025-04-28 21:21:44,947 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 386 states to 386 states and 2907 transitions.
[2025-04-28 21:21:44,947 INFO  L79                 Accepts]: Start accepts. Automaton has 386 states and 2907 transitions. Word has length 18
[2025-04-28 21:21:44,947 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,947 INFO  L485      AbstractCegarLoop]: Abstraction has 386 states and 2907 transitions.
[2025-04-28 21:21:44,948 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:44,948 INFO  L278                IsEmpty]: Start isEmpty. Operand 386 states and 2907 transitions.
[2025-04-28 21:21:44,969 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:44,969 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,969 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,970 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:44,970 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,971 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,972 INFO  L85        PathProgramCache]: Analyzing trace with hash 1391677287, now seen corresponding path program 1 times
[2025-04-28 21:21:44,972 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,972 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [716034787]
[2025-04-28 21:21:44,972 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,972 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,993 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:45,023 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:45,024 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,024 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,457 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:45,457 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,457 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [716034787]
[2025-04-28 21:21:45,457 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [716034787] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,457 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,457 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:45,458 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [905321851]
[2025-04-28 21:21:45,458 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,458 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:45,458 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,459 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:45,459 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:45,459 INFO  L87              Difference]: Start difference. First operand 386 states and 2907 transitions. Second operand  has 5 states, 4 states have (on average 1.5) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:47,018 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,019 INFO  L93              Difference]: Finished difference Result 483 states and 4152 transitions.
[2025-04-28 21:21:47,019 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:47,020 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:21:47,020 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,059 INFO  L225             Difference]: With dead ends: 483
[2025-04-28 21:21:47,060 INFO  L226             Difference]: Without dead ends: 483
[2025-04-28 21:21:47,060 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:47,061 INFO  L437           NwaCegarLoop]: 241 mSDtfsCounter, 1 mSDsluCounter, 552 mSDsCounter, 0 mSdLazyCounter, 746 mSolverCounterSat, 58 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 97 SdHoareTripleChecker+Valid, 793 SdHoareTripleChecker+Invalid, 804 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 58 IncrementalHoareTripleChecker+Valid, 746 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,062 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [97 Valid, 793 Invalid, 804 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [58 Valid, 746 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-04-28 21:21:47,063 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 483 states.
[2025-04-28 21:21:47,871 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 483 to 449.
[2025-04-28 21:21:47,875 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 449 states, 44 states have (on average 1.1590909090909092) internal successors, (51), 41 states have internal predecessors, (51), 379 states have call successors, (470), 19 states have call predecessors, (470), 34 states have return successors, (3385), 393 states have call predecessors, (3385), 379 states have call successors, (3385)
[2025-04-28 21:21:47,898 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 449 states to 449 states and 3906 transitions.
[2025-04-28 21:21:47,898 INFO  L79                 Accepts]: Start accepts. Automaton has 449 states and 3906 transitions. Word has length 21
[2025-04-28 21:21:47,898 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,898 INFO  L485      AbstractCegarLoop]: Abstraction has 449 states and 3906 transitions.
[2025-04-28 21:21:47,898 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:47,899 INFO  L278                IsEmpty]: Start isEmpty. Operand 449 states and 3906 transitions.
[2025-04-28 21:21:47,920 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:47,920 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,921 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,921 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:47,921 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,922 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,922 INFO  L85        PathProgramCache]: Analyzing trace with hash 1783358954, now seen corresponding path program 1 times
[2025-04-28 21:21:47,922 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,922 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [366823945]
[2025-04-28 21:21:47,922 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,922 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,944 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:47,974 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:47,974 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,974 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,515 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:48,515 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,515 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [366823945]
[2025-04-28 21:21:48,515 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [366823945] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,516 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,516 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:48,516 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [989464893]
[2025-04-28 21:21:48,516 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,516 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:48,516 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,517 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:48,517 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:48,517 INFO  L87              Difference]: Start difference. First operand 449 states and 3906 transitions. Second operand  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:50,518 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,519 INFO  L93              Difference]: Finished difference Result 802 states and 10803 transitions.
[2025-04-28 21:21:50,519 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:50,519 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:21:50,520 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,604 INFO  L225             Difference]: With dead ends: 802
[2025-04-28 21:21:50,605 INFO  L226             Difference]: Without dead ends: 802
[2025-04-28 21:21:50,605 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:50,605 INFO  L437           NwaCegarLoop]: 224 mSDtfsCounter, 1 mSDsluCounter, 726 mSDsCounter, 0 mSdLazyCounter, 878 mSolverCounterSat, 89 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 147 SdHoareTripleChecker+Valid, 950 SdHoareTripleChecker+Invalid, 967 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 89 IncrementalHoareTripleChecker+Valid, 878 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,606 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [147 Valid, 950 Invalid, 967 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [89 Valid, 878 Invalid, 0 Unknown, 0 Unchecked, 1.8s Time]
[2025-04-28 21:21:50,607 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 802 states.
[2025-04-28 21:21:52,721 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 802 to 788.
[2025-04-28 21:21:52,732 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 788 states, 71 states have (on average 1.1690140845070423) internal successors, (83), 63 states have internal predecessors, (83), 674 states have call successors, (809), 28 states have call predecessors, (809), 56 states have return successors, (9738), 701 states have call predecessors, (9738), 674 states have call successors, (9738)
[2025-04-28 21:21:52,816 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 788 states to 788 states and 10630 transitions.
[2025-04-28 21:21:52,817 INFO  L79                 Accepts]: Start accepts. Automaton has 788 states and 10630 transitions. Word has length 21
[2025-04-28 21:21:52,818 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,820 INFO  L485      AbstractCegarLoop]: Abstraction has 788 states and 10630 transitions.
[2025-04-28 21:21:52,824 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:52,824 INFO  L278                IsEmpty]: Start isEmpty. Operand 788 states and 10630 transitions.
[2025-04-28 21:21:52,865 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:52,865 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,866 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,866 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:52,866 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,867 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,867 INFO  L85        PathProgramCache]: Analyzing trace with hash -1701184175, now seen corresponding path program 1 times
[2025-04-28 21:21:52,867 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,868 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [799049612]
[2025-04-28 21:21:52,868 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,868 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,893 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:52,920 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:52,920 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,921 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,174 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:53,174 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,175 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [799049612]
[2025-04-28 21:21:53,175 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [799049612] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,175 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,175 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:53,175 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [526013001]
[2025-04-28 21:21:53,175 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,175 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:53,177 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,177 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:53,177 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:53,177 INFO  L87              Difference]: Start difference. First operand 788 states and 10630 transitions. Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:55,068 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,068 INFO  L93              Difference]: Finished difference Result 1168 states and 15920 transitions.
[2025-04-28 21:21:55,069 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:55,069 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:21:55,069 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,176 INFO  L225             Difference]: With dead ends: 1168
[2025-04-28 21:21:55,176 INFO  L226             Difference]: Without dead ends: 1168
[2025-04-28 21:21:55,176 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,177 INFO  L437           NwaCegarLoop]: 314 mSDtfsCounter, 2 mSDsluCounter, 1044 mSDsCounter, 0 mSdLazyCounter, 929 mSolverCounterSat, 69 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 99 SdHoareTripleChecker+Valid, 1358 SdHoareTripleChecker+Invalid, 998 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 69 IncrementalHoareTripleChecker+Valid, 929 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,177 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [99 Valid, 1358 Invalid, 998 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [69 Valid, 929 Invalid, 0 Unknown, 0 Unchecked, 1.7s Time]
[2025-04-28 21:21:55,179 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1168 states.
