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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:15,090 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:15,179 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_71916c32-62ec-48d1-8e03-4661df6709b7/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:15,183 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:15,184 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:15,220 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:15,221 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:15,221 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:15,221 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:15,222 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:15,223 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:15,223 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:15,223 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:15,223 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:15,224 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:15,224 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:15,224 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:15,225 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:15,225 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:15,225 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:15,225 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:15,225 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:15,225 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:15,225 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:15,225 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:15,226 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:15,226 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:15,554 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:15,565 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:15,567 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:15,570 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:15,571 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:15,572 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_71916c32-62ec-48d1-8e03-4661df6709b7/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-119.smt2
[2025-04-28 21:21:15,573 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:15,579 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:15,896 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_71916c32-62ec-48d1-8e03-4661df6709b7/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-119.smt2
[2025-04-28 21:21:15,901 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:15,903 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:15,905 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:15,905 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:15,905 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:15,907 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,933 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15 Unit
[2025-04-28 21:21:15,933 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:15,935 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,935 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:15,935 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:15,951 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,951 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,971 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,971 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,976 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,977 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,980 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,981 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,982 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,994 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,998 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:15,998 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:15,998 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:16,000 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:16,002 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:16,016 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:16,030 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:16,036 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:16,051 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:16,051 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:16,052 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:16,052 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Inv given in one single declaration
[2025-04-28 21:21:16,052 INFO  L130     BoogieDeclarations]: Found specification of procedure Inv
[2025-04-28 21:21:16,052 INFO  L138     BoogieDeclarations]: Found implementation of procedure Inv
[2025-04-28 21:21:16,052 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:16,052 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:16,052 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:16,104 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:16,106 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:16,448 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:16,449 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:16,470 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:16,471 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:16,471 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:16 BoogieIcfgContainer
[2025-04-28 21:21:16,472 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:16,476 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:16,476 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:16,483 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:16,483 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/3) ...
[2025-04-28 21:21:16,484 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@40ab8619 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:16, skipping insertion in model container
[2025-04-28 21:21:16,484 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (2/3) ...
[2025-04-28 21:21:16,484 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@40ab8619 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:16, skipping insertion in model container
[2025-04-28 21:21:16,485 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:16" (3/3) ...
[2025-04-28 21:21:16,487 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:16,508 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:16,511 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 54 locations, 172 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:16,573 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:16,591 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;@555ed366, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:16,592 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:16,597 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 54 states, 6 states have (on average 5.666666666666667) internal successors, (34), 34 states have internal predecessors, (34), 45 states have call successors, (46), 2 states have call predecessors, (46), 2 states have return successors, (46), 19 states have call predecessors, (46), 45 states have call successors, (46)
[2025-04-28 21:21:16,635 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-04-28 21:21:16,638 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,639 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-04-28 21:21:16,639 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,648 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,648 INFO  L85        PathProgramCache]: Analyzing trace with hash 270999585, now seen corresponding path program 1 times
[2025-04-28 21:21:16,657 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,659 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [246873706]
[2025-04-28 21:21:16,659 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,661 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,679 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-04-28 21:21:16,681 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-04-28 21:21:16,681 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,681 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,716 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:16,716 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,717 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [246873706]
[2025-04-28 21:21:16,717 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [246873706] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,717 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,724 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-04-28 21:21:16,725 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [407908139]
[2025-04-28 21:21:16,726 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,728 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-04-28 21:21:16,729 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,758 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-04-28 21:21:16,758 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-04-28 21:21:16,760 INFO  L87              Difference]: Start difference. First operand  has 54 states, 6 states have (on average 5.666666666666667) internal successors, (34), 34 states have internal predecessors, (34), 45 states have call successors, (46), 2 states have call predecessors, (46), 2 states have return successors, (46), 19 states have call predecessors, (46), 45 states have call successors, (46) 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:16,801 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,801 INFO  L93              Difference]: Finished difference Result 52 states and 123 transitions.
[2025-04-28 21:21:16,803 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-04-28 21:21:16,805 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:16,805 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,817 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:16,818 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:16,819 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:16,822 INFO  L437           NwaCegarLoop]: 123 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, 123 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:16,823 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 123 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:16,838 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:16,876 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 52.
[2025-04-28 21:21:16,878 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 5 states have (on average 6.2) internal successors, (31), 31 states have internal predecessors, (31), 45 states have call successors, (46), 2 states have call predecessors, (46), 2 states have return successors, (46), 19 states have call predecessors, (46), 45 states have call successors, (46)
[2025-04-28 21:21:16,888 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 123 transitions.
[2025-04-28 21:21:16,890 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 123 transitions. Word has length 5
[2025-04-28 21:21:16,890 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,893 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 123 transitions.
[2025-04-28 21:21:16,893 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:16,893 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 123 transitions.
[2025-04-28 21:21:16,905 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:16,905 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,905 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,905 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:16,906 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,906 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,906 INFO  L85        PathProgramCache]: Analyzing trace with hash -2080238469, now seen corresponding path program 1 times
[2025-04-28 21:21:16,906 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,907 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [705234652]
[2025-04-28 21:21:16,907 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,907 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,916 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:16,964 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:16,964 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,964 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,075 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:17,075 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,075 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [705234652]
[2025-04-28 21:21:17,075 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [705234652] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,075 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,076 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:17,076 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1015952591]
[2025-04-28 21:21:17,076 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,077 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:17,077 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,078 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:17,078 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,078 INFO  L87              Difference]: Start difference. First operand 52 states and 123 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:17,954 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,955 INFO  L93              Difference]: Finished difference Result 92 states and 272 transitions.
[2025-04-28 21:21:17,955 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:17,956 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:17,956 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,971 INFO  L225             Difference]: With dead ends: 92
[2025-04-28 21:21:17,974 INFO  L226             Difference]: Without dead ends: 92
[2025-04-28 21:21:17,975 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:17,976 INFO  L437           NwaCegarLoop]: 145 mSDtfsCounter, 22 mSDsluCounter, 167 mSDsCounter, 0 mSdLazyCounter, 256 mSolverCounterSat, 77 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 33 SdHoareTripleChecker+Valid, 312 SdHoareTripleChecker+Invalid, 333 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 77 IncrementalHoareTripleChecker+Valid, 256 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,976 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [33 Valid, 312 Invalid, 333 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [77 Valid, 256 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:17,977 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-04-28 21:21:18,025 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 92.
[2025-04-28 21:21:18,026 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 7 states have (on average 7.714285714285714) internal successors, (54), 53 states have internal predecessors, (54), 83 states have call successors, (85), 3 states have call predecessors, (85), 3 states have return successors, (133), 36 states have call predecessors, (133), 83 states have call successors, (133)
[2025-04-28 21:21:18,036 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 272 transitions.
[2025-04-28 21:21:18,036 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 272 transitions. Word has length 9
[2025-04-28 21:21:18,037 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,037 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 272 transitions.
[2025-04-28 21:21:18,037 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:18,038 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 272 transitions.
[2025-04-28 21:21:18,054 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:18,054 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,054 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,054 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:18,054 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,055 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,055 INFO  L85        PathProgramCache]: Analyzing trace with hash 70355162, now seen corresponding path program 1 times
[2025-04-28 21:21:18,055 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,056 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1220827460]
[2025-04-28 21:21:18,056 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,056 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,061 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:18,072 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:18,072 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,072 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,183 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:18,183 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,184 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1220827460]
[2025-04-28 21:21:18,184 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1220827460] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:18,184 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [38357206]
[2025-04-28 21:21:18,185 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,185 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:18,187 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:18,193 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:18,195 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:18,237 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:18,252 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:18,253 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,253 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,255 INFO  L256         TraceCheckSpWp]: Trace formula consists of 68 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:18,261 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:18,318 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:18,318 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:18,500 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:18,501 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [38357206] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:18,501 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:18,501 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 5
[2025-04-28 21:21:18,501 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [860113218]
[2025-04-28 21:21:18,501 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,501 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:18,502 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,502 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:18,503 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:18,503 INFO  L87              Difference]: Start difference. First operand 92 states and 272 transitions. Second operand  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:20,278 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,279 INFO  L93              Difference]: Finished difference Result 257 states and 1189 transitions.
[2025-04-28 21:21:20,279 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:20,280 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:20,280 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,319 INFO  L225             Difference]: With dead ends: 257
[2025-04-28 21:21:20,319 INFO  L226             Difference]: Without dead ends: 257
[2025-04-28 21:21:20,320 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 30 GetRequests, 23 SyntacticMatches, 3 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:20,320 INFO  L437           NwaCegarLoop]: 134 mSDtfsCounter, 90 mSDsluCounter, 220 mSDsCounter, 0 mSdLazyCounter, 546 mSolverCounterSat, 359 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 132 SdHoareTripleChecker+Valid, 354 SdHoareTripleChecker+Invalid, 905 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 359 IncrementalHoareTripleChecker+Valid, 546 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,321 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [132 Valid, 354 Invalid, 905 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [359 Valid, 546 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:21:20,322 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 257 states.
[2025-04-28 21:21:20,441 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 257 to 177.
[2025-04-28 21:21:20,442 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 177 states, 11 states have (on average 9.545454545454545) internal successors, (105), 102 states have internal predecessors, (105), 164 states have call successors, (168), 5 states have call predecessors, (168), 5 states have return successors, (400), 70 states have call predecessors, (400), 164 states have call successors, (400)
[2025-04-28 21:21:20,451 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 177 states to 177 states and 673 transitions.
[2025-04-28 21:21:20,452 INFO  L79                 Accepts]: Start accepts. Automaton has 177 states and 673 transitions. Word has length 12
[2025-04-28 21:21:20,453 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,453 INFO  L485      AbstractCegarLoop]: Abstraction has 177 states and 673 transitions.
[2025-04-28 21:21:20,453 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:20,453 INFO  L278                IsEmpty]: Start isEmpty. Operand 177 states and 673 transitions.
[2025-04-28 21:21:20,475 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:20,475 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,476 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,482 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:20,677 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:20,678 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,678 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,678 INFO  L85        PathProgramCache]: Analyzing trace with hash 864433705, now seen corresponding path program 1 times
[2025-04-28 21:21:20,678 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,679 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1149007628]
[2025-04-28 21:21:20,679 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,679 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,683 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:20,692 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:20,692 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,693 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,742 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:20,742 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,742 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1149007628]
[2025-04-28 21:21:20,743 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1149007628] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,743 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,743 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:20,743 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2067985354]
[2025-04-28 21:21:20,743 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,743 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:20,743 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,744 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:20,744 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:20,744 INFO  L87              Difference]: Start difference. First operand 177 states and 673 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:21,383 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,383 INFO  L93              Difference]: Finished difference Result 337 states and 1731 transitions.
[2025-04-28 21:21:21,384 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:21,384 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:21,384 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,440 INFO  L225             Difference]: With dead ends: 337
[2025-04-28 21:21:21,440 INFO  L226             Difference]: Without dead ends: 337
[2025-04-28 21:21:21,440 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:21,441 INFO  L437           NwaCegarLoop]: 180 mSDtfsCounter, 22 mSDsluCounter, 202 mSDsCounter, 0 mSdLazyCounter, 253 mSolverCounterSat, 77 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 39 SdHoareTripleChecker+Valid, 382 SdHoareTripleChecker+Invalid, 330 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 77 IncrementalHoareTripleChecker+Valid, 253 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,441 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [39 Valid, 382 Invalid, 330 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [77 Valid, 253 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:21,445 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 337 states.
[2025-04-28 21:21:21,639 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 337 to 337.
[2025-04-28 21:21:21,641 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 337 states, 19 states have (on average 10.578947368421053) internal successors, (201), 190 states have internal predecessors, (201), 316 states have call successors, (324), 9 states have call predecessors, (324), 9 states have return successors, (1206), 138 states have call predecessors, (1206), 316 states have call successors, (1206)
[2025-04-28 21:21:21,661 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 337 states to 337 states and 1731 transitions.
[2025-04-28 21:21:21,662 INFO  L79                 Accepts]: Start accepts. Automaton has 337 states and 1731 transitions. Word has length 13
[2025-04-28 21:21:21,662 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,662 INFO  L485      AbstractCegarLoop]: Abstraction has 337 states and 1731 transitions.
[2025-04-28 21:21:21,662 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:21,662 INFO  L278                IsEmpty]: Start isEmpty. Operand 337 states and 1731 transitions.
[2025-04-28 21:21:21,688 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:21,688 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,688 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,689 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:21,689 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,689 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,689 INFO  L85        PathProgramCache]: Analyzing trace with hash 1254332489, now seen corresponding path program 1 times
[2025-04-28 21:21:21,689 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,690 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1872852189]
[2025-04-28 21:21:21,690 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,690 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,697 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:21,706 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:21,706 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,706 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,794 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:21,795 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,795 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1872852189]
[2025-04-28 21:21:21,795 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1872852189] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,796 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,796 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:21,796 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1519407608]
[2025-04-28 21:21:21,796 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,796 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:21,796 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,797 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:21,797 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:21,797 INFO  L87              Difference]: Start difference. First operand 337 states and 1731 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:22,689 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:22,690 INFO  L93              Difference]: Finished difference Result 521 states and 5584 transitions.
[2025-04-28 21:21:22,690 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:22,691 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:22,691 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:22,909 INFO  L225             Difference]: With dead ends: 521
[2025-04-28 21:21:22,909 INFO  L226             Difference]: Without dead ends: 521
[2025-04-28 21:21:22,909 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:22,910 INFO  L437           NwaCegarLoop]: 148 mSDtfsCounter, 23 mSDsluCounter, 154 mSDsCounter, 0 mSdLazyCounter, 343 mSolverCounterSat, 101 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 74 SdHoareTripleChecker+Valid, 302 SdHoareTripleChecker+Invalid, 444 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 101 IncrementalHoareTripleChecker+Valid, 343 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:22,910 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [74 Valid, 302 Invalid, 444 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [101 Valid, 343 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:22,912 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 521 states.
[2025-04-28 21:21:23,494 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 521 to 497.
[2025-04-28 21:21:23,498 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 497 states, 27 states have (on average 10.777777777777779) internal successors, (291), 278 states have internal predecessors, (291), 468 states have call successors, (480), 13 states have call predecessors, (480), 13 states have return successors, (2401), 206 states have call predecessors, (2401), 468 states have call successors, (2401)
[2025-04-28 21:21:23,549 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 497 states to 497 states and 3172 transitions.
[2025-04-28 21:21:23,549 INFO  L79                 Accepts]: Start accepts. Automaton has 497 states and 3172 transitions. Word has length 13
[2025-04-28 21:21:23,550 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,550 INFO  L485      AbstractCegarLoop]: Abstraction has 497 states and 3172 transitions.
[2025-04-28 21:21:23,550 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:23,550 INFO  L278                IsEmpty]: Start isEmpty. Operand 497 states and 3172 transitions.
[2025-04-28 21:21:23,602 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:23,603 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,603 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:23,603 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:23,603 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,604 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,604 INFO  L85        PathProgramCache]: Analyzing trace with hash -1264724432, now seen corresponding path program 1 times
[2025-04-28 21:21:23,604 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,604 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1838706826]
[2025-04-28 21:21:23,604 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,604 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,610 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:23,623 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:23,624 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,624 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,697 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:23,697 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,698 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1838706826]
[2025-04-28 21:21:23,698 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1838706826] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:23,698 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1951348575]
[2025-04-28 21:21:23,698 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,698 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:23,701 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:23,703 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:23,707 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:23,742 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:23,759 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:23,759 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,759 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,760 INFO  L256         TraceCheckSpWp]: Trace formula consists of 98 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:23,762 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:23,799 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:23,799 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:24,049 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:24,049 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1951348575] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:24,049 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:24,049 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-04-28 21:21:24,049 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1094592765]
[2025-04-28 21:21:24,050 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:24,050 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:24,050 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:24,050 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:24,051 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:24,051 INFO  L87              Difference]: Start difference. First operand 497 states and 3172 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:27,622 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,622 INFO  L93              Difference]: Finished difference Result 545 states and 7834 transitions.
[2025-04-28 21:21:27,623 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:27,623 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 16
[2025-04-28 21:21:27,623 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,776 INFO  L225             Difference]: With dead ends: 545
[2025-04-28 21:21:27,776 INFO  L226             Difference]: Without dead ends: 545
[2025-04-28 21:21:27,777 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 44 GetRequests, 31 SyntacticMatches, 2 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 21 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=54, Invalid=102, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:27,777 INFO  L437           NwaCegarLoop]: 143 mSDtfsCounter, 101 mSDsluCounter, 163 mSDsCounter, 0 mSdLazyCounter, 902 mSolverCounterSat, 660 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 361 SdHoareTripleChecker+Valid, 306 SdHoareTripleChecker+Invalid, 1562 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 660 IncrementalHoareTripleChecker+Valid, 902 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 3.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,778 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [361 Valid, 306 Invalid, 1562 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [660 Valid, 902 Invalid, 0 Unknown, 0 Unchecked, 3.3s Time]
[2025-04-28 21:21:27,779 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 545 states.
[2025-04-28 21:21:28,389 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 545 to 337.
[2025-04-28 21:21:28,391 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 337 states, 19 states have (on average 10.578947368421053) internal successors, (201), 190 states have internal predecessors, (201), 316 states have call successors, (324), 9 states have call predecessors, (324), 9 states have return successors, (1170), 138 states have call predecessors, (1170), 316 states have call successors, (1170)
[2025-04-28 21:21:28,412 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 337 states to 337 states and 1695 transitions.
[2025-04-28 21:21:28,412 INFO  L79                 Accepts]: Start accepts. Automaton has 337 states and 1695 transitions. Word has length 16
[2025-04-28 21:21:28,412 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,412 INFO  L485      AbstractCegarLoop]: Abstraction has 337 states and 1695 transitions.
[2025-04-28 21:21:28,412 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:28,412 INFO  L278                IsEmpty]: Start isEmpty. Operand 337 states and 1695 transitions.
[2025-04-28 21:21:28,439 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:28,439 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,440 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:28,445 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:28,643 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,644 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,646 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,646 INFO  L85        PathProgramCache]: Analyzing trace with hash -1875158921, now seen corresponding path program 1 times
[2025-04-28 21:21:28,646 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,646 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [797347400]
[2025-04-28 21:21:28,646 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:28,646 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,650 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:28,656 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:28,656 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,656 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,723 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:28,724 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,724 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [797347400]
[2025-04-28 21:21:28,724 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [797347400] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:28,724 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:28,724 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:28,724 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1649411168]
[2025-04-28 21:21:28,724 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,725 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:28,725 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,725 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:28,725 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:28,726 INFO  L87              Difference]: Start difference. First operand 337 states and 1695 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:29,574 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,574 INFO  L93              Difference]: Finished difference Result 689 states and 8270 transitions.
[2025-04-28 21:21:29,575 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:29,575 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:21:29,575 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,839 INFO  L225             Difference]: With dead ends: 689
[2025-04-28 21:21:29,839 INFO  L226             Difference]: Without dead ends: 689
[2025-04-28 21:21:29,839 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:29,840 INFO  L437           NwaCegarLoop]: 141 mSDtfsCounter, 23 mSDsluCounter, 142 mSDsCounter, 0 mSdLazyCounter, 329 mSolverCounterSat, 117 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 71 SdHoareTripleChecker+Valid, 283 SdHoareTripleChecker+Invalid, 446 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 117 IncrementalHoareTripleChecker+Valid, 329 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,841 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [71 Valid, 283 Invalid, 446 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [117 Valid, 329 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:29,842 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 689 states.
[2025-04-28 21:21:30,563 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 689 to 657.
[2025-04-28 21:21:30,568 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 657 states, 35 states have (on average 11.17142857142857) internal successors, (391), 366 states have internal predecessors, (391), 620 states have call successors, (636), 17 states have call predecessors, (636), 17 states have return successors, (3614), 274 states have call predecessors, (3614), 620 states have call successors, (3614)
[2025-04-28 21:21:30,629 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 657 states to 657 states and 4641 transitions.
[2025-04-28 21:21:30,629 INFO  L79                 Accepts]: Start accepts. Automaton has 657 states and 4641 transitions. Word has length 17
[2025-04-28 21:21:30,629 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,629 INFO  L485      AbstractCegarLoop]: Abstraction has 657 states and 4641 transitions.
[2025-04-28 21:21:30,630 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:30,630 INFO  L278                IsEmpty]: Start isEmpty. Operand 657 states and 4641 transitions.
[2025-04-28 21:21:30,689 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:30,689 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,689 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,690 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:30,690 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,690 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,690 INFO  L85        PathProgramCache]: Analyzing trace with hash 1755787722, now seen corresponding path program 1 times
[2025-04-28 21:21:30,691 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,691 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [150448621]
[2025-04-28 21:21:30,691 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,691 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,701 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:30,707 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:30,707 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,707 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,758 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:30,759 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,759 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [150448621]
[2025-04-28 21:21:30,759 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [150448621] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,759 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:30,760 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:30,760 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1610540538]
[2025-04-28 21:21:30,760 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,760 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:30,760 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,761 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:30,761 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:30,762 INFO  L87              Difference]: Start difference. First operand 657 states and 4641 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:31,680 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,680 INFO  L93              Difference]: Finished difference Result 857 states and 12230 transitions.
[2025-04-28 21:21:31,680 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:31,681 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 17
[2025-04-28 21:21:31,681 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,221 INFO  L225             Difference]: With dead ends: 857
[2025-04-28 21:21:32,221 INFO  L226             Difference]: Without dead ends: 857
[2025-04-28 21:21:32,222 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:32,223 INFO  L437           NwaCegarLoop]: 153 mSDtfsCounter, 23 mSDsluCounter, 178 mSDsCounter, 0 mSdLazyCounter, 311 mSolverCounterSat, 88 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 72 SdHoareTripleChecker+Valid, 331 SdHoareTripleChecker+Invalid, 399 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 88 IncrementalHoareTripleChecker+Valid, 311 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,223 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [72 Valid, 331 Invalid, 399 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [88 Valid, 311 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:32,225 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 857 states.
[2025-04-28 21:21:33,335 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 857 to 817.
[2025-04-28 21:21:33,341 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 817 states, 43 states have (on average 11.186046511627907) internal successors, (481), 454 states have internal predecessors, (481), 772 states have call successors, (792), 21 states have call predecessors, (792), 21 states have return successors, (5469), 342 states have call predecessors, (5469), 772 states have call successors, (5469)
[2025-04-28 21:21:33,440 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 817 states to 817 states and 6742 transitions.
[2025-04-28 21:21:33,440 INFO  L79                 Accepts]: Start accepts. Automaton has 817 states and 6742 transitions. Word has length 17
[2025-04-28 21:21:33,440 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,440 INFO  L485      AbstractCegarLoop]: Abstraction has 817 states and 6742 transitions.
[2025-04-28 21:21:33,441 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:33,441 INFO  L278                IsEmpty]: Start isEmpty. Operand 817 states and 6742 transitions.
[2025-04-28 21:21:33,486 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:33,486 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,486 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,487 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:33,487 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,487 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,488 INFO  L85        PathProgramCache]: Analyzing trace with hash 1982019151, now seen corresponding path program 1 times
[2025-04-28 21:21:33,488 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,488 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [639336666]
[2025-04-28 21:21:33,488 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,488 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,493 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:33,497 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:33,497 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,497 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,557 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 8 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:33,557 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,557 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [639336666]
[2025-04-28 21:21:33,557 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [639336666] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,557 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1907204106]
[2025-04-28 21:21:33,557 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,557 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,560 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,563 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:33,569 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,601 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:33,619 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:33,619 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,619 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,620 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,621 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,645 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 8 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:33,646 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,881 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 8 proven. 2 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:33,881 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1907204106] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,881 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,881 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-04-28 21:21:33,881 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [157243307]
[2025-04-28 21:21:33,881 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,882 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:33,882 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,882 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:33,882 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:33,883 INFO  L87              Difference]: Start difference. First operand 817 states and 6742 transitions. Second operand  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:36,943 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,944 INFO  L93              Difference]: Finished difference Result 897 states and 16962 transitions.
[2025-04-28 21:21:36,944 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:36,944 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6) Word has length 20
[2025-04-28 21:21:36,944 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,350 INFO  L225             Difference]: With dead ends: 897
[2025-04-28 21:21:37,350 INFO  L226             Difference]: Without dead ends: 897
[2025-04-28 21:21:37,350 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 52 GetRequests, 39 SyntacticMatches, 2 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 20 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=54, Invalid=102, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:37,351 INFO  L437           NwaCegarLoop]: 150 mSDtfsCounter, 97 mSDsluCounter, 283 mSDsCounter, 0 mSdLazyCounter, 1193 mSolverCounterSat, 368 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 181 SdHoareTripleChecker+Valid, 433 SdHoareTripleChecker+Invalid, 1561 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 368 IncrementalHoareTripleChecker+Valid, 1193 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,351 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [181 Valid, 433 Invalid, 1561 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [368 Valid, 1193 Invalid, 0 Unknown, 0 Unchecked, 2.7s Time]
[2025-04-28 21:21:37,352 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 897 states.
[2025-04-28 21:21:38,660 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 897 to 657.
[2025-04-28 21:21:38,666 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 657 states, 35 states have (on average 11.17142857142857) internal successors, (391), 366 states have internal predecessors, (391), 620 states have call successors, (636), 17 states have call predecessors, (636), 17 states have return successors, (3410), 274 states have call predecessors, (3410), 620 states have call successors, (3410)
[2025-04-28 21:21:38,732 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 657 states to 657 states and 4437 transitions.
[2025-04-28 21:21:38,732 INFO  L79                 Accepts]: Start accepts. Automaton has 657 states and 4437 transitions. Word has length 20
[2025-04-28 21:21:38,732 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,732 INFO  L485      AbstractCegarLoop]: Abstraction has 657 states and 4437 transitions.
[2025-04-28 21:21:38,732 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.5) internal successors, (10), 6 states have internal predecessors, (10), 3 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:38,733 INFO  L278                IsEmpty]: Start isEmpty. Operand 657 states and 4437 transitions.
[2025-04-28 21:21:38,780 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:38,780 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,780 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,786 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:38,982 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,983 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,984 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,984 INFO  L85        PathProgramCache]: Analyzing trace with hash -443959816, now seen corresponding path program 1 times
[2025-04-28 21:21:38,984 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,985 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1790838739]
[2025-04-28 21:21:38,985 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,985 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,001 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:39,012 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:39,013 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,013 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,115 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:39,115 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,115 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1790838739]
[2025-04-28 21:21:39,116 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1790838739] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,116 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,116 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:39,116 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [970703709]
[2025-04-28 21:21:39,116 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,117 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:39,117 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,118 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:39,118 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:39,118 INFO  L87              Difference]: Start difference. First operand 657 states and 4437 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:40,003 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,003 INFO  L93              Difference]: Finished difference Result 1257 states and 16422 transitions.
[2025-04-28 21:21:40,003 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:40,004 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5) Word has length 21
[2025-04-28 21:21:40,004 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,572 INFO  L225             Difference]: With dead ends: 1257
[2025-04-28 21:21:40,572 INFO  L226             Difference]: Without dead ends: 1185
[2025-04-28 21:21:40,573 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:40,573 INFO  L437           NwaCegarLoop]: 155 mSDtfsCounter, 20 mSDsluCounter, 155 mSDsCounter, 0 mSdLazyCounter, 318 mSolverCounterSat, 99 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 59 SdHoareTripleChecker+Valid, 310 SdHoareTripleChecker+Invalid, 417 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 99 IncrementalHoareTripleChecker+Valid, 318 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,574 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [59 Valid, 310 Invalid, 417 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [99 Valid, 318 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:40,575 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1185 states.
[2025-04-28 21:21:41,637 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1185 to 801.
[2025-04-28 21:21:41,651 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 801 states, 55 states have (on average 8.309090909090909) internal successors, (457), 430 states have internal predecessors, (457), 732 states have call successors, (752), 21 states have call predecessors, (752), 33 states have return successors, (6559), 350 states have call predecessors, (6559), 732 states have call successors, (6559)
[2025-04-28 21:21:41,748 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 801 states to 801 states and 7768 transitions.
[2025-04-28 21:21:41,749 INFO  L79                 Accepts]: Start accepts. Automaton has 801 states and 7768 transitions. Word has length 21
[2025-04-28 21:21:41,749 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,749 INFO  L485      AbstractCegarLoop]: Abstraction has 801 states and 7768 transitions.
[2025-04-28 21:21:41,752 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 2 states have call successors, (5), 1 states have call predecessors, (5), 2 states have return successors, (5), 1 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:41,752 INFO  L278                IsEmpty]: Start isEmpty. Operand 801 states and 7768 transitions.
[2025-04-28 21:21:41,805 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-04-28 21:21:41,805 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,805 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,805 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:41,805 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,806 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,806 INFO  L85        PathProgramCache]: Analyzing trace with hash 1804418867, now seen corresponding path program 1 times
[2025-04-28 21:21:41,806 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,807 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [44581483]
[2025-04-28 21:21:41,807 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,807 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,813 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:41,817 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:41,821 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,821 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,907 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:41,907 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,907 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [44581483]
[2025-04-28 21:21:41,907 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [44581483] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,908 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,908 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:41,908 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1918642403]
[2025-04-28 21:21:41,908 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,908 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:41,908 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,908 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:41,908 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:41,909 INFO  L87              Difference]: Start difference. First operand 801 states and 7768 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:42,642 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,643 INFO  L93              Difference]: Finished difference Result 1021 states and 10688 transitions.
[2025-04-28 21:21:42,643 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:42,644 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 23
[2025-04-28 21:21:42,644 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,721 INFO  L225             Difference]: With dead ends: 1021
[2025-04-28 21:21:42,721 INFO  L226             Difference]: Without dead ends: 656
[2025-04-28 21:21:42,721 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:42,721 INFO  L437           NwaCegarLoop]: 170 mSDtfsCounter, 20 mSDsluCounter, 144 mSDsCounter, 0 mSdLazyCounter, 223 mSolverCounterSat, 148 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 62 SdHoareTripleChecker+Valid, 314 SdHoareTripleChecker+Invalid, 371 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 148 IncrementalHoareTripleChecker+Valid, 223 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,722 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [62 Valid, 314 Invalid, 371 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [148 Valid, 223 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:42,723 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 656 states.
[2025-04-28 21:21:43,053 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 656 to 575.
[2025-04-28 21:21:43,060 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 575 states, 39 states have (on average 12.538461538461538) internal successors, (489), 408 states have internal predecessors, (489), 550 states have call successors, (576), 27 states have call predecessors, (576), 11 states have return successors, (1329), 140 states have call predecessors, (1329), 550 states have call successors, (1329)
[2025-04-28 21:21:43,083 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 575 states to 575 states and 2394 transitions.
[2025-04-28 21:21:43,083 INFO  L79                 Accepts]: Start accepts. Automaton has 575 states and 2394 transitions. Word has length 23
[2025-04-28 21:21:43,084 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,084 INFO  L485      AbstractCegarLoop]: Abstraction has 575 states and 2394 transitions.
[2025-04-28 21:21:43,085 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:43,085 INFO  L278                IsEmpty]: Start isEmpty. Operand 575 states and 2394 transitions.
[2025-04-28 21:21:43,099 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-04-28 21:21:43,099 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,100 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,100 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:43,100 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,101 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,101 INFO  L85        PathProgramCache]: Analyzing trace with hash -1916340135, now seen corresponding path program 1 times
[2025-04-28 21:21:43,101 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,101 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1823192640]
[2025-04-28 21:21:43,101 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,101 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,107 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:43,114 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:43,115 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,115 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,153 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:43,155 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,155 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1823192640]
[2025-04-28 21:21:43,155 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1823192640] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,155 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,155 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:43,155 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2025116172]
[2025-04-28 21:21:43,155 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,156 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:43,156 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,156 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:43,156 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:43,156 INFO  L87              Difference]: Start difference. First operand 575 states and 2394 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:43,656 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,656 INFO  L93              Difference]: Finished difference Result 624 states and 4038 transitions.
[2025-04-28 21:21:43,656 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:43,656 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 23
[2025-04-28 21:21:43,657 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,755 INFO  L225             Difference]: With dead ends: 624
[2025-04-28 21:21:43,756 INFO  L226             Difference]: Without dead ends: 624
[2025-04-28 21:21:43,756 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:43,756 INFO  L437           NwaCegarLoop]: 116 mSDtfsCounter, 14 mSDsluCounter, 135 mSDsCounter, 0 mSdLazyCounter, 226 mSolverCounterSat, 82 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 57 SdHoareTripleChecker+Valid, 251 SdHoareTripleChecker+Invalid, 308 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 82 IncrementalHoareTripleChecker+Valid, 226 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,757 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [57 Valid, 251 Invalid, 308 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [82 Valid, 226 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:43,758 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 624 states.
[2025-04-28 21:21:44,061 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 624 to 602.
[2025-04-28 21:21:44,068 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 602 states, 41 states have (on average 12.292682926829269) internal successors, (504), 421 states have internal predecessors, (504), 575 states have call successors, (602), 28 states have call predecessors, (602), 12 states have return successors, (1461), 153 states have call predecessors, (1461), 575 states have call successors, (1461)
[2025-04-28 21:21:44,099 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 602 states to 602 states and 2567 transitions.
[2025-04-28 21:21:44,100 INFO  L79                 Accepts]: Start accepts. Automaton has 602 states and 2567 transitions. Word has length 23
[2025-04-28 21:21:44,100 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,100 INFO  L485      AbstractCegarLoop]: Abstraction has 602 states and 2567 transitions.
[2025-04-28 21:21:44,100 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:44,100 INFO  L278                IsEmpty]: Start isEmpty. Operand 602 states and 2567 transitions.
[2025-04-28 21:21:44,125 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-04-28 21:21:44,125 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,125 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:44,125 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:44,126 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,126 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,126 INFO  L85        PathProgramCache]: Analyzing trace with hash 1950178858, now seen corresponding path program 1 times
[2025-04-28 21:21:44,127 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,127 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2108144541]
[2025-04-28 21:21:44,127 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,127 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,136 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-04-28 21:21:44,143 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-04-28 21:21:44,144 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,144 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
