./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-144.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:29,225 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:29,307 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f3264992-7e26-44e3-9a17-8ce4431e7607/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:29,312 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:29,312 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:29,335 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:29,336 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:29,336 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:29,336 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:29,336 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:29,337 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:29,338 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:29,338 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:29,338 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:29,338 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:29,340 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:29,340 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:29,340 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:29,340 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:29,340 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:29,341 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:29,341 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:29,341 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:29,341 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:29,341 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:29,342 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:29,342 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:29,688 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:29,701 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:29,704 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:29,707 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:29,708 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:29,711 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f3264992-7e26-44e3-9a17-8ce4431e7607/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-144.smt2
[2025-04-28 21:21:29,715 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:29,719 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:30,578 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f3264992-7e26-44e3-9a17-8ce4431e7607/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-144.smt2
[2025-04-28 21:21:30,582 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:30,585 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:30,586 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:30,587 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:30,587 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:30,590 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,674 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30 Unit
[2025-04-28 21:21:30,677 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:30,679 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:30,679 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:30,679 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:30,703 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,703 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,743 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,743 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,752 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,756 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,758 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,763 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,765 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,786 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:30,787 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:30,787 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:30,787 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:30,789 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:30,791 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:30,806 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,825 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:30,828 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:30,844 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:30,845 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:30,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:30,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_42 given in one single declaration
[2025-04-28 21:21:30,845 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_42
[2025-04-28 21:21:30,845 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_42
[2025-04-28 21:21:30,845 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:30,846 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:30,846 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:30,917 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:30,920 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:31,781 INFO  L?                        ?]: Removed 430 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:31,782 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:31,799 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:31,801 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:31,802 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:31 BoogieIcfgContainer
[2025-04-28 21:21:31,802 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:31,808 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:31,809 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:31,813 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:31,816 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:30" (1/3) ...
[2025-04-28 21:21:31,818 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5d1cdfcf and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:31, skipping insertion in model container
[2025-04-28 21:21:31,818 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:30" (2/3) ...
[2025-04-28 21:21:31,818 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5d1cdfcf and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:31, skipping insertion in model container
[2025-04-28 21:21:31,818 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:31" (3/3) ...
[2025-04-28 21:21:31,820 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:31,838 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:31,842 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 41 locations, 129 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:31,909 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:31,932 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;@7e3241e7, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:31,932 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:31,937 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 41 states, 6 states have (on average 6.0) internal successors, (36), 36 states have internal predecessors, (36), 31 states have call successors, (31), 2 states have call predecessors, (31), 2 states have return successors, (31), 3 states have call predecessors, (31), 31 states have call successors, (31)
[2025-04-28 21:21:31,980 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:31,983 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,984 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,984 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,990 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,990 INFO  L85        PathProgramCache]: Analyzing trace with hash -2069245614, now seen corresponding path program 1 times
[2025-04-28 21:21:32,002 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,003 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [841050370]
[2025-04-28 21:21:32,003 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,004 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,033 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:32,052 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:32,052 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,052 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,214 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:32,217 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,217 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [841050370]
[2025-04-28 21:21:32,218 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [841050370] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,218 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:32,222 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:32,224 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [231091475]
[2025-04-28 21:21:32,226 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,231 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:32,233 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,270 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:32,271 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:32,273 INFO  L87              Difference]: Start difference. First operand  has 41 states, 6 states have (on average 6.0) internal successors, (36), 36 states have internal predecessors, (36), 31 states have call successors, (31), 2 states have call predecessors, (31), 2 states have return successors, (31), 3 states have call predecessors, (31), 31 states have call successors, (31) 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:32,826 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,829 INFO  L93              Difference]: Finished difference Result 41 states and 126 transitions.
[2025-04-28 21:21:32,830 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:32,831 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:32,833 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,846 INFO  L225             Difference]: With dead ends: 41
[2025-04-28 21:21:32,847 INFO  L226             Difference]: Without dead ends: 41
[2025-04-28 21:21:32,850 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:32,853 INFO  L437           NwaCegarLoop]: 67 mSDtfsCounter, 1 mSDsluCounter, 80 mSDsCounter, 0 mSdLazyCounter, 137 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 147 SdHoareTripleChecker+Invalid, 146 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 137 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,857 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 147 Invalid, 146 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 137 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:32,895 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 41 states.
[2025-04-28 21:21:32,993 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 41 to 41.
[2025-04-28 21:21:32,995 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 6 states have (on average 5.833333333333333) internal successors, (35), 35 states have internal predecessors, (35), 31 states have call successors, (31), 2 states have call predecessors, (31), 3 states have return successors, (60), 4 states have call predecessors, (60), 31 states have call successors, (60)
[2025-04-28 21:21:33,009 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 126 transitions.
[2025-04-28 21:21:33,010 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 126 transitions. Word has length 9
[2025-04-28 21:21:33,015 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,015 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 126 transitions.
[2025-04-28 21:21:33,015 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:33,016 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 126 transitions.
[2025-04-28 21:21:33,023 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:33,023 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,023 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,024 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:33,024 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,025 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,025 INFO  L85        PathProgramCache]: Analyzing trace with hash -431508629, now seen corresponding path program 1 times
[2025-04-28 21:21:33,025 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,025 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1717988548]
[2025-04-28 21:21:33,025 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,026 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,032 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:33,060 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:33,061 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,061 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,380 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:33,380 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,380 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1717988548]
[2025-04-28 21:21:33,380 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1717988548] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,381 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1694336947]
[2025-04-28 21:21:33,381 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,381 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,385 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,390 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:33,392 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,440 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:33,464 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:33,464 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,464 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,469 INFO  L256         TraceCheckSpWp]: Trace formula consists of 83 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,473 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,598 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:33,598 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,961 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:33,961 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1694336947] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,962 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,962 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:33,963 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [633423787]
[2025-04-28 21:21:33,963 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,963 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:33,965 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,965 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:33,966 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=66, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:33,966 INFO  L87              Difference]: Start difference. First operand 41 states and 126 transitions. Second operand  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:35,411 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,411 INFO  L93              Difference]: Finished difference Result 55 states and 339 transitions.
[2025-04-28 21:21:35,413 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:35,414 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 13
[2025-04-28 21:21:35,414 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,427 INFO  L225             Difference]: With dead ends: 55
[2025-04-28 21:21:35,427 INFO  L226             Difference]: Without dead ends: 55
[2025-04-28 21:21:35,428 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=31, Invalid=79, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:35,429 INFO  L437           NwaCegarLoop]: 69 mSDtfsCounter, 4 mSDsluCounter, 175 mSDsCounter, 0 mSdLazyCounter, 995 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 244 SdHoareTripleChecker+Invalid, 1008 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 995 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,429 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 244 Invalid, 1008 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 995 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:35,430 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 55 states.
[2025-04-28 21:21:35,512 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 55 to 47.
[2025-04-28 21:21:35,512 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 47 states, 9 states have (on average 4.222222222222222) internal successors, (38), 38 states have internal predecessors, (38), 31 states have call successors, (31), 2 states have call predecessors, (31), 6 states have return successors, (148), 6 states have call predecessors, (148), 31 states have call successors, (148)
[2025-04-28 21:21:35,515 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 47 states to 47 states and 217 transitions.
[2025-04-28 21:21:35,515 INFO  L79                 Accepts]: Start accepts. Automaton has 47 states and 217 transitions. Word has length 13
[2025-04-28 21:21:35,516 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,516 INFO  L485      AbstractCegarLoop]: Abstraction has 47 states and 217 transitions.
[2025-04-28 21:21:35,516 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:35,516 INFO  L278                IsEmpty]: Start isEmpty. Operand 47 states and 217 transitions.
[2025-04-28 21:21:35,521 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:35,521 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,521 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,527 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:35,725 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:35,726 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,726 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,727 INFO  L85        PathProgramCache]: Analyzing trace with hash -110856442, now seen corresponding path program 1 times
[2025-04-28 21:21:35,727 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,727 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [938438318]
[2025-04-28 21:21:35,727 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,727 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,734 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:35,755 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:35,755 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,755 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,921 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:35,921 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,921 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [938438318]
[2025-04-28 21:21:35,921 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [938438318] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,921 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:35,922 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:35,922 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [373005836]
[2025-04-28 21:21:35,922 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,922 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:35,922 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,923 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:35,923 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:35,923 INFO  L87              Difference]: Start difference. First operand 47 states and 217 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:36,713 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,713 INFO  L93              Difference]: Finished difference Result 69 states and 439 transitions.
[2025-04-28 21:21:36,714 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:36,714 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 13
[2025-04-28 21:21:36,714 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,724 INFO  L225             Difference]: With dead ends: 69
[2025-04-28 21:21:36,724 INFO  L226             Difference]: Without dead ends: 69
[2025-04-28 21:21:36,724 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:36,725 INFO  L437           NwaCegarLoop]: 81 mSDtfsCounter, 15 mSDsluCounter, 14 mSDsCounter, 0 mSdLazyCounter, 343 mSolverCounterSat, 23 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 68 SdHoareTripleChecker+Valid, 95 SdHoareTripleChecker+Invalid, 366 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 23 IncrementalHoareTripleChecker+Valid, 343 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,725 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [68 Valid, 95 Invalid, 366 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [23 Valid, 343 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:36,726 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 69 states.
[2025-04-28 21:21:36,787 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 69 to 67.
[2025-04-28 21:21:36,788 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 67 states, 13 states have (on average 5.461538461538462) internal successors, (71), 54 states have internal predecessors, (71), 44 states have call successors, (44), 3 states have call predecessors, (44), 9 states have return successors, (284), 9 states have call predecessors, (284), 44 states have call successors, (284)
[2025-04-28 21:21:36,794 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 67 states to 67 states and 399 transitions.
[2025-04-28 21:21:36,795 INFO  L79                 Accepts]: Start accepts. Automaton has 67 states and 399 transitions. Word has length 13
[2025-04-28 21:21:36,795 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,795 INFO  L485      AbstractCegarLoop]: Abstraction has 67 states and 399 transitions.
[2025-04-28 21:21:36,795 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:36,795 INFO  L278                IsEmpty]: Start isEmpty. Operand 67 states and 399 transitions.
[2025-04-28 21:21:36,809 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:36,809 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,809 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,809 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:36,810 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,810 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,810 INFO  L85        PathProgramCache]: Analyzing trace with hash -2028716542, now seen corresponding path program 1 times
[2025-04-28 21:21:36,810 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,810 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2097392354]
[2025-04-28 21:21:36,810 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,811 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,822 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:36,833 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:36,833 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,833 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,977 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:36,978 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,978 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2097392354]
[2025-04-28 21:21:36,978 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2097392354] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,978 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2069166502]
[2025-04-28 21:21:36,978 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,978 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,981 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,984 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:36,988 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,027 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:37,044 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:37,044 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,044 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,046 INFO  L256         TraceCheckSpWp]: Trace formula consists of 67 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,048 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,093 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:37,094 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:37,398 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:37,399 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2069166502] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,399 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:37,399 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [6, 6] total 8
[2025-04-28 21:21:37,399 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [844217281]
[2025-04-28 21:21:37,399 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,399 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:37,399 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,400 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:37,400 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:37,400 INFO  L87              Difference]: Start difference. First operand 67 states and 399 transitions. Second operand  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 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:38,548 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,548 INFO  L93              Difference]: Finished difference Result 82 states and 649 transitions.
[2025-04-28 21:21:38,549 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:38,549 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 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:38,549 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,558 INFO  L225             Difference]: With dead ends: 82
[2025-04-28 21:21:38,558 INFO  L226             Difference]: Without dead ends: 82
[2025-04-28 21:21:38,558 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 31 GetRequests, 21 SyntacticMatches, 4 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:38,559 INFO  L437           NwaCegarLoop]: 79 mSDtfsCounter, 12 mSDsluCounter, 66 mSDsCounter, 0 mSdLazyCounter, 739 mSolverCounterSat, 35 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 94 SdHoareTripleChecker+Valid, 145 SdHoareTripleChecker+Invalid, 774 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 35 IncrementalHoareTripleChecker+Valid, 739 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,560 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [94 Valid, 145 Invalid, 774 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [35 Valid, 739 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:21:38,561 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 82 states.
[2025-04-28 21:21:38,630 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 82 to 78.
[2025-04-28 21:21:38,631 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 18 states have (on average 4.055555555555555) internal successors, (73), 61 states have internal predecessors, (73), 45 states have call successors, (45), 3 states have call predecessors, (45), 14 states have return successors, (449), 13 states have call predecessors, (449), 45 states have call successors, (449)
[2025-04-28 21:21:38,637 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 567 transitions.
[2025-04-28 21:21:38,637 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 567 transitions. Word has length 13
[2025-04-28 21:21:38,637 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,637 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 567 transitions.
[2025-04-28 21:21:38,637 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 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:38,637 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 567 transitions.
[2025-04-28 21:21:38,647 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:38,647 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,647 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,653 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:38,851 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,852 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,852 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,853 INFO  L85        PathProgramCache]: Analyzing trace with hash -356107295, now seen corresponding path program 1 times
[2025-04-28 21:21:38,853 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,853 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [302402204]
[2025-04-28 21:21:38,853 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,853 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,858 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:38,863 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:38,863 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,863 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,925 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:38,925 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,925 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [302402204]
[2025-04-28 21:21:38,925 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [302402204] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:38,925 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,925 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:38,925 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1807034691]
[2025-04-28 21:21:38,925 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,926 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:38,926 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,926 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:38,926 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:38,927 INFO  L87              Difference]: Start difference. First operand 78 states and 567 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:39,398 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,398 INFO  L93              Difference]: Finished difference Result 84 states and 680 transitions.
[2025-04-28 21:21:39,398 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:39,399 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 13
[2025-04-28 21:21:39,399 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,406 INFO  L225             Difference]: With dead ends: 84
[2025-04-28 21:21:39,406 INFO  L226             Difference]: Without dead ends: 84
[2025-04-28 21:21:39,407 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:39,407 INFO  L437           NwaCegarLoop]: 72 mSDtfsCounter, 1 mSDsluCounter, 19 mSDsCounter, 0 mSdLazyCounter, 270 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 91 SdHoareTripleChecker+Invalid, 282 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 270 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,408 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 91 Invalid, 282 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 270 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:39,409 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 84 states.
[2025-04-28 21:21:39,485 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 84 to 82.
[2025-04-28 21:21:39,486 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 20 states have (on average 3.75) internal successors, (75), 63 states have internal predecessors, (75), 45 states have call successors, (45), 3 states have call predecessors, (45), 16 states have return successors, (516), 15 states have call predecessors, (516), 45 states have call successors, (516)
[2025-04-28 21:21:39,490 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 636 transitions.
[2025-04-28 21:21:39,490 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 636 transitions. Word has length 13
[2025-04-28 21:21:39,491 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,491 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 636 transitions.
[2025-04-28 21:21:39,491 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:39,491 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 636 transitions.
[2025-04-28 21:21:39,501 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:39,501 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,502 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,502 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:39,502 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,502 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,502 INFO  L85        PathProgramCache]: Analyzing trace with hash -601358148, now seen corresponding path program 1 times
[2025-04-28 21:21:39,503 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,503 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1924897104]
[2025-04-28 21:21:39,503 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,503 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,508 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:39,519 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:39,519 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,520 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,658 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:39,660 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,660 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1924897104]
[2025-04-28 21:21:39,660 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1924897104] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,660 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:39,661 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:39,661 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [239532089]
[2025-04-28 21:21:39,661 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,661 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:39,661 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,662 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:39,662 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:39,662 INFO  L87              Difference]: Start difference. First operand 82 states and 636 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:40,367 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,367 INFO  L93              Difference]: Finished difference Result 94 states and 768 transitions.
[2025-04-28 21:21:40,368 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:40,368 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:40,368 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,376 INFO  L225             Difference]: With dead ends: 94
[2025-04-28 21:21:40,376 INFO  L226             Difference]: Without dead ends: 94
[2025-04-28 21:21:40,376 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:40,378 INFO  L437           NwaCegarLoop]: 81 mSDtfsCounter, 12 mSDsluCounter, 18 mSDsCounter, 0 mSdLazyCounter, 323 mSolverCounterSat, 32 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 54 SdHoareTripleChecker+Valid, 99 SdHoareTripleChecker+Invalid, 355 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 32 IncrementalHoareTripleChecker+Valid, 323 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,378 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [54 Valid, 99 Invalid, 355 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [32 Valid, 323 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:40,381 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-04-28 21:21:40,487 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 84.
[2025-04-28 21:21:40,487 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 21 states have (on average 3.619047619047619) internal successors, (76), 64 states have internal predecessors, (76), 45 states have call successors, (45), 3 states have call predecessors, (45), 17 states have return successors, (490), 16 states have call predecessors, (490), 45 states have call successors, (490)
[2025-04-28 21:21:40,495 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 611 transitions.
[2025-04-28 21:21:40,495 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 611 transitions. Word has length 13
[2025-04-28 21:21:40,495 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,495 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 611 transitions.
[2025-04-28 21:21:40,496 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:40,496 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 611 transitions.
[2025-04-28 21:21:40,513 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:40,513 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,513 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,513 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:40,514 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,514 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,514 INFO  L85        PathProgramCache]: Analyzing trace with hash -846609001, now seen corresponding path program 1 times
[2025-04-28 21:21:40,514 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,514 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1657909184]
[2025-04-28 21:21:40,514 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,515 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,521 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:40,575 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:40,576 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,576 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,747 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:40,748 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,748 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1657909184]
[2025-04-28 21:21:40,748 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1657909184] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,748 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1018355002]
[2025-04-28 21:21:40,748 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,749 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,751 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,753 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:40,756 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,797 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:40,814 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:40,814 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,814 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,815 INFO  L256         TraceCheckSpWp]: Trace formula consists of 107 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,816 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,882 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:40,882 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:41,173 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:41,174 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1018355002] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:41,174 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:41,174 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:41,174 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1755858291]
[2025-04-28 21:21:41,174 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,174 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:41,174 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,175 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:41,175 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=66, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:41,175 INFO  L87              Difference]: Start difference. First operand 84 states and 611 transitions. Second operand  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:41,861 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,861 INFO  L93              Difference]: Finished difference Result 102 states and 928 transitions.
[2025-04-28 21:21:41,862 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:41,862 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 13
[2025-04-28 21:21:41,862 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,870 INFO  L225             Difference]: With dead ends: 102
[2025-04-28 21:21:41,871 INFO  L226             Difference]: Without dead ends: 102
[2025-04-28 21:21:41,871 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=38, Invalid=94, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:41,873 INFO  L437           NwaCegarLoop]: 74 mSDtfsCounter, 8 mSDsluCounter, 117 mSDsCounter, 0 mSdLazyCounter, 458 mSolverCounterSat, 37 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 191 SdHoareTripleChecker+Invalid, 495 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 37 IncrementalHoareTripleChecker+Valid, 458 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,873 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 191 Invalid, 495 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [37 Valid, 458 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:41,874 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 102 states.
[2025-04-28 21:21:41,991 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 102 to 88.
[2025-04-28 21:21:41,992 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 88 states, 23 states have (on average 3.391304347826087) internal successors, (78), 66 states have internal predecessors, (78), 45 states have call successors, (45), 3 states have call predecessors, (45), 19 states have return successors, (564), 18 states have call predecessors, (564), 45 states have call successors, (564)
[2025-04-28 21:21:41,996 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 88 states to 88 states and 687 transitions.
[2025-04-28 21:21:41,996 INFO  L79                 Accepts]: Start accepts. Automaton has 88 states and 687 transitions. Word has length 13
[2025-04-28 21:21:41,996 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,996 INFO  L485      AbstractCegarLoop]: Abstraction has 88 states and 687 transitions.
[2025-04-28 21:21:41,997 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:41,997 INFO  L278                IsEmpty]: Start isEmpty. Operand 88 states and 687 transitions.
[2025-04-28 21:21:42,008 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:42,008 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,008 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,013 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:42,209 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,209 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,210 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,210 INFO  L85        PathProgramCache]: Analyzing trace with hash -698832844, now seen corresponding path program 1 times
[2025-04-28 21:21:42,210 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,210 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1079256077]
[2025-04-28 21:21:42,210 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,210 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,218 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:42,226 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:42,226 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,226 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,310 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:42,311 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,311 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1079256077]
[2025-04-28 21:21:42,311 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1079256077] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,311 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [486940037]
[2025-04-28 21:21:42,311 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,311 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,313 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,316 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:42,319 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,356 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:42,369 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:42,369 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,369 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,370 INFO  L256         TraceCheckSpWp]: Trace formula consists of 66 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,371 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,421 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:42,421 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:42,641 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:42,642 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [486940037] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:42,642 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:42,642 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:42,645 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [765089575]
[2025-04-28 21:21:42,645 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,646 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:42,646 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,646 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:42,646 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:42,646 INFO  L87              Difference]: Start difference. First operand 88 states and 687 transitions. Second operand  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:43,496 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,496 INFO  L93              Difference]: Finished difference Result 112 states and 1083 transitions.
[2025-04-28 21:21:43,497 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:43,497 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7) Word has length 13
[2025-04-28 21:21:43,497 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,517 INFO  L225             Difference]: With dead ends: 112
[2025-04-28 21:21:43,517 INFO  L226             Difference]: Without dead ends: 112
[2025-04-28 21:21:43,517 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=31, Invalid=79, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:43,518 INFO  L437           NwaCegarLoop]: 71 mSDtfsCounter, 3 mSDsluCounter, 177 mSDsCounter, 0 mSdLazyCounter, 793 mSolverCounterSat, 30 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 248 SdHoareTripleChecker+Invalid, 823 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 30 IncrementalHoareTripleChecker+Valid, 793 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,518 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 248 Invalid, 823 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [30 Valid, 793 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:43,519 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-04-28 21:21:43,629 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 94.
[2025-04-28 21:21:43,630 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 26 states have (on average 3.1153846153846154) internal successors, (81), 69 states have internal predecessors, (81), 45 states have call successors, (45), 3 states have call predecessors, (45), 22 states have return successors, (673), 21 states have call predecessors, (673), 45 states have call successors, (673)
[2025-04-28 21:21:43,634 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 799 transitions.
[2025-04-28 21:21:43,634 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 799 transitions. Word has length 13
[2025-04-28 21:21:43,634 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,634 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 799 transitions.
[2025-04-28 21:21:43,634 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 6 states have (on average 2.0) internal successors, (12), 9 states have internal predecessors, (12), 5 states have call successors, (5), 1 states have call predecessors, (5), 5 states have return successors, (7), 3 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:43,635 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 799 transitions.
[2025-04-28 21:21:43,644 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:43,644 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,644 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,650 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:43,848 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,849 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,850 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,850 INFO  L85        PathProgramCache]: Analyzing trace with hash 1530498195, now seen corresponding path program 1 times
[2025-04-28 21:21:43,850 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,850 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [196054464]
[2025-04-28 21:21:43,850 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,850 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,853 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:43,856 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:43,856 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,856 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,979 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:43,979 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,979 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [196054464]
[2025-04-28 21:21:43,979 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [196054464] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,979 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1309918652]
[2025-04-28 21:21:43,979 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,980 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,982 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,984 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:43,989 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,027 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:44,036 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:44,037 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,037 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,038 INFO  L256         TraceCheckSpWp]: Trace formula consists of 71 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,039 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,093 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:44,093 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,326 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:44,326 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1309918652] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,326 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,326 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:44,326 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1647570940]
[2025-04-28 21:21:44,326 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,327 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:44,327 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,327 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:44,327 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=24, Invalid=66, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:44,327 INFO  L87              Difference]: Start difference. First operand 94 states and 799 transitions. Second operand  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:45,021 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,021 INFO  L93              Difference]: Finished difference Result 112 states and 1081 transitions.
[2025-04-28 21:21:45,022 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:45,022 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 13
[2025-04-28 21:21:45,022 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,030 INFO  L225             Difference]: With dead ends: 112
[2025-04-28 21:21:45,030 INFO  L226             Difference]: Without dead ends: 112
[2025-04-28 21:21:45,030 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 23 SyntacticMatches, 0 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=31, Invalid=79, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:45,031 INFO  L437           NwaCegarLoop]: 75 mSDtfsCounter, 6 mSDsluCounter, 132 mSDsCounter, 0 mSdLazyCounter, 590 mSolverCounterSat, 37 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 207 SdHoareTripleChecker+Invalid, 627 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 37 IncrementalHoareTripleChecker+Valid, 590 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,031 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 207 Invalid, 627 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [37 Valid, 590 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:45,031 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-04-28 21:21:45,168 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 94.
[2025-04-28 21:21:45,169 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 26 states have (on average 3.1153846153846154) internal successors, (81), 69 states have internal predecessors, (81), 45 states have call successors, (45), 3 states have call predecessors, (45), 22 states have return successors, (673), 21 states have call predecessors, (673), 45 states have call successors, (673)
[2025-04-28 21:21:45,173 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 799 transitions.
[2025-04-28 21:21:45,173 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 799 transitions. Word has length 13
[2025-04-28 21:21:45,173 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,173 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 799 transitions.
[2025-04-28 21:21:45,173 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:45,174 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 799 transitions.
[2025-04-28 21:21:45,183 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:45,183 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,183 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,189 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:45,387 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,388 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,392 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,393 INFO  L85        PathProgramCache]: Analyzing trace with hash -1657762894, now seen corresponding path program 1 times
[2025-04-28 21:21:45,393 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,393 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1154019105]
[2025-04-28 21:21:45,393 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,393 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,398 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:45,404 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:45,404 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,404 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,482 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:45,482 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,483 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1154019105]
[2025-04-28 21:21:45,483 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1154019105] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,483 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,483 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:45,483 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1351726769]
[2025-04-28 21:21:45,484 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,484 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:45,484 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,485 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:45,485 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:45,485 INFO  L87              Difference]: Start difference. First operand 94 states and 799 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:46,241 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,242 INFO  L93              Difference]: Finished difference Result 98 states and 846 transitions.
[2025-04-28 21:21:46,242 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:46,242 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:46,243 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,250 INFO  L225             Difference]: With dead ends: 98
[2025-04-28 21:21:46,250 INFO  L226             Difference]: Without dead ends: 98
[2025-04-28 21:21:46,250 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:46,251 INFO  L437           NwaCegarLoop]: 84 mSDtfsCounter, 11 mSDsluCounter, 17 mSDsCounter, 0 mSdLazyCounter, 366 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 53 SdHoareTripleChecker+Valid, 101 SdHoareTripleChecker+Invalid, 394 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 366 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,251 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [53 Valid, 101 Invalid, 394 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 366 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:46,252 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 98 states.
[2025-04-28 21:21:46,333 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 98 to 94.
[2025-04-28 21:21:46,334 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 26 states have (on average 3.1153846153846154) internal successors, (81), 69 states have internal predecessors, (81), 45 states have call successors, (45), 3 states have call predecessors, (45), 22 states have return successors, (643), 21 states have call predecessors, (643), 45 states have call successors, (643)
[2025-04-28 21:21:46,340 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 769 transitions.
[2025-04-28 21:21:46,341 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 769 transitions. Word has length 13
[2025-04-28 21:21:46,341 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,341 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 769 transitions.
[2025-04-28 21:21:46,341 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:46,341 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 769 transitions.
[2025-04-28 21:21:46,351 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:46,352 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,352 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,353 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:46,353 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,354 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,354 INFO  L85        PathProgramCache]: Analyzing trace with hash 1039996489, now seen corresponding path program 1 times
[2025-04-28 21:21:46,354 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,354 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1638295005]
[2025-04-28 21:21:46,354 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,354 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,358 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:46,365 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:46,367 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,367 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,409 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:46,409 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,409 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1638295005]
[2025-04-28 21:21:46,410 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1638295005] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:46,410 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:46,410 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:46,410 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2074102952]
[2025-04-28 21:21:46,410 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,410 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:46,412 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,412 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:46,413 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:46,413 INFO  L87              Difference]: Start difference. First operand 94 states and 769 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:47,041 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,042 INFO  L93              Difference]: Finished difference Result 104 states and 852 transitions.
[2025-04-28 21:21:47,043 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:47,043 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:47,043 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,050 INFO  L225             Difference]: With dead ends: 104
[2025-04-28 21:21:47,050 INFO  L226             Difference]: Without dead ends: 104
[2025-04-28 21:21:47,051 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:47,052 INFO  L437           NwaCegarLoop]: 85 mSDtfsCounter, 12 mSDsluCounter, 19 mSDsCounter, 0 mSdLazyCounter, 335 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 55 SdHoareTripleChecker+Valid, 104 SdHoareTripleChecker+Invalid, 363 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 335 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,052 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [55 Valid, 104 Invalid, 363 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 335 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:47,053 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 104 states.
[2025-04-28 21:21:47,126 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 104 to 94.
[2025-04-28 21:21:47,127 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 26 states have (on average 3.1153846153846154) internal successors, (81), 69 states have internal predecessors, (81), 45 states have call successors, (45), 3 states have call predecessors, (45), 22 states have return successors, (613), 21 states have call predecessors, (613), 45 states have call successors, (613)
[2025-04-28 21:21:47,130 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 739 transitions.
[2025-04-28 21:21:47,130 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 739 transitions. Word has length 13
[2025-04-28 21:21:47,131 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,131 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 739 transitions.
[2025-04-28 21:21:47,131 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:47,131 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 739 transitions.
[2025-04-28 21:21:47,139 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:47,139 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,140 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,140 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:47,140 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,140 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,140 INFO  L85        PathProgramCache]: Analyzing trace with hash 1115397823, now seen corresponding path program 1 times
[2025-04-28 21:21:47,140 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,140 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [291875349]
[2025-04-28 21:21:47,140 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,141 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,146 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:47,153 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:47,153 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,153 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,267 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:47,268 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,268 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [291875349]
[2025-04-28 21:21:47,269 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [291875349] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,269 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,269 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:47,269 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [758988117]
[2025-04-28 21:21:47,269 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,269 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:47,269 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,270 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:47,270 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:47,270 INFO  L87              Difference]: Start difference. First operand 94 states and 739 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:47,841 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,841 INFO  L93              Difference]: Finished difference Result 104 states and 753 transitions.
[2025-04-28 21:21:47,841 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:47,841 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:47,841 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,847 INFO  L225             Difference]: With dead ends: 104
[2025-04-28 21:21:47,847 INFO  L226             Difference]: Without dead ends: 104
[2025-04-28 21:21:47,848 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 5 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:47,848 INFO  L437           NwaCegarLoop]: 92 mSDtfsCounter, 12 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 315 mSolverCounterSat, 35 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 47 SdHoareTripleChecker+Valid, 113 SdHoareTripleChecker+Invalid, 350 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 35 IncrementalHoareTripleChecker+Valid, 315 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,848 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [47 Valid, 113 Invalid, 350 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [35 Valid, 315 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:47,849 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 104 states.
[2025-04-28 21:21:47,902 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 104 to 94.
[2025-04-28 21:21:47,903 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 94 states, 26 states have (on average 3.1153846153846154) internal successors, (81), 69 states have internal predecessors, (81), 45 states have call successors, (45), 3 states have call predecessors, (45), 22 states have return successors, (523), 21 states have call predecessors, (523), 45 states have call successors, (523)
[2025-04-28 21:21:47,906 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 94 states to 94 states and 649 transitions.
[2025-04-28 21:21:47,906 INFO  L79                 Accepts]: Start accepts. Automaton has 94 states and 649 transitions. Word has length 13
[2025-04-28 21:21:47,906 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,906 INFO  L485      AbstractCegarLoop]: Abstraction has 94 states and 649 transitions.
[2025-04-28 21:21:47,907 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:47,907 INFO  L278                IsEmpty]: Start isEmpty. Operand 94 states and 649 transitions.
[2025-04-28 21:21:47,914 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:47,914 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,914 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:47,914 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:47,914 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,916 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,916 INFO  L85        PathProgramCache]: Analyzing trace with hash 328077050, now seen corresponding path program 1 times
[2025-04-28 21:21:47,917 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,917 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2070234654]
[2025-04-28 21:21:47,917 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,917 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,923 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:47,932 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:47,932 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,932 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,036 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:48,036 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,036 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2070234654]
[2025-04-28 21:21:48,036 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2070234654] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,036 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,037 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:48,037 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [441594088]
[2025-04-28 21:21:48,037 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,037 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:48,037 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,038 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:48,038 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:48,038 INFO  L87              Difference]: Start difference. First operand 94 states and 649 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:48,565 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,565 INFO  L93              Difference]: Finished difference Result 125 states and 823 transitions.
[2025-04-28 21:21:48,565 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:48,566 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:48,566 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,572 INFO  L225             Difference]: With dead ends: 125
[2025-04-28 21:21:48,572 INFO  L226             Difference]: Without dead ends: 125
[2025-04-28 21:21:48,572 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:48,573 INFO  L437           NwaCegarLoop]: 101 mSDtfsCounter, 8 mSDsluCounter, 43 mSDsCounter, 0 mSdLazyCounter, 216 mSolverCounterSat, 71 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 144 SdHoareTripleChecker+Invalid, 287 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 71 IncrementalHoareTripleChecker+Valid, 216 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,573 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 144 Invalid, 287 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [71 Valid, 216 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:48,574 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 125 states.
[2025-04-28 21:21:48,622 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 125 to 101.
[2025-04-28 21:21:48,623 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 101 states, 27 states have (on average 4.111111111111111) internal successors, (111), 76 states have internal predecessors, (111), 51 states have call successors, (51), 4 states have call predecessors, (51), 22 states have return successors, (414), 20 states have call predecessors, (414), 51 states have call successors, (414)
[2025-04-28 21:21:48,625 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 101 states to 101 states and 576 transitions.
[2025-04-28 21:21:48,626 INFO  L79                 Accepts]: Start accepts. Automaton has 101 states and 576 transitions. Word has length 17
[2025-04-28 21:21:48,626 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:48,626 INFO  L485      AbstractCegarLoop]: Abstraction has 101 states and 576 transitions.
[2025-04-28 21:21:48,626 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:48,626 INFO  L278                IsEmpty]: Start isEmpty. Operand 101 states and 576 transitions.
[2025-04-28 21:21:48,633 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:48,633 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:48,633 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:48,633 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:48,633 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:48,634 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:48,634 INFO  L85        PathProgramCache]: Analyzing trace with hash 1938270461, now seen corresponding path program 1 times
[2025-04-28 21:21:48,634 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:48,634 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [218956023]
[2025-04-28 21:21:48,634 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:48,634 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:48,638 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:48,643 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:48,643 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:48,643 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,684 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:48,684 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:48,684 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [218956023]
[2025-04-28 21:21:48,684 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [218956023] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:48,684 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:48,684 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:48,684 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1246757115]
[2025-04-28 21:21:48,684 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,685 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:48,685 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,686 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:48,686 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:48,686 INFO  L87              Difference]: Start difference. First operand 101 states and 576 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:49,168 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,168 INFO  L93              Difference]: Finished difference Result 115 states and 645 transitions.
[2025-04-28 21:21:49,169 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:49,169 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:49,169 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,173 INFO  L225             Difference]: With dead ends: 115
[2025-04-28 21:21:49,173 INFO  L226             Difference]: Without dead ends: 115
[2025-04-28 21:21:49,174 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:49,174 INFO  L437           NwaCegarLoop]: 107 mSDtfsCounter, 9 mSDsluCounter, 51 mSDsCounter, 0 mSdLazyCounter, 225 mSolverCounterSat, 45 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 38 SdHoareTripleChecker+Valid, 158 SdHoareTripleChecker+Invalid, 270 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 45 IncrementalHoareTripleChecker+Valid, 225 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,174 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [38 Valid, 158 Invalid, 270 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [45 Valid, 225 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:49,175 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 115 states.
[2025-04-28 21:21:49,209 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 115 to 101.
[2025-04-28 21:21:49,210 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 101 states, 27 states have (on average 4.111111111111111) internal successors, (111), 76 states have internal predecessors, (111), 51 states have call successors, (51), 4 states have call predecessors, (51), 22 states have return successors, (367), 20 states have call predecessors, (367), 51 states have call successors, (367)
[2025-04-28 21:21:49,213 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 101 states to 101 states and 529 transitions.
[2025-04-28 21:21:49,213 INFO  L79                 Accepts]: Start accepts. Automaton has 101 states and 529 transitions. Word has length 17
[2025-04-28 21:21:49,213 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,214 INFO  L485      AbstractCegarLoop]: Abstraction has 101 states and 529 transitions.
[2025-04-28 21:21:49,214 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:49,214 INFO  L278                IsEmpty]: Start isEmpty. Operand 101 states and 529 transitions.
[2025-04-28 21:21:49,221 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:49,221 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,221 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:49,221 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:49,222 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,222 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,222 INFO  L85        PathProgramCache]: Analyzing trace with hash -927381150, now seen corresponding path program 1 times
[2025-04-28 21:21:49,222 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,222 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1083417360]
[2025-04-28 21:21:49,222 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,223 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,227 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:49,233 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:49,233 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,234 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,308 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:49,308 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,308 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1083417360]
[2025-04-28 21:21:49,308 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1083417360] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:49,308 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1933534746]
[2025-04-28 21:21:49,308 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,308 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,311 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,313 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:49,316 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:49,358 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:49,379 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:49,379 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,379 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,380 INFO  L256         TraceCheckSpWp]: Trace formula consists of 133 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:49,383 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:49,417 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:49,417 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:49,417 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1933534746] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,417 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:49,417 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [6] total 8
[2025-04-28 21:21:49,417 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [229843593]
[2025-04-28 21:21:49,417 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,417 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:49,418 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,418 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:49,418 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:49,418 INFO  L87              Difference]: Start difference. First operand 101 states and 529 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:49,858 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,859 INFO  L93              Difference]: Finished difference Result 119 states and 634 transitions.
[2025-04-28 21:21:49,859 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:49,860 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:49,860 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,864 INFO  L225             Difference]: With dead ends: 119
[2025-04-28 21:21:49,865 INFO  L226             Difference]: Without dead ends: 119
[2025-04-28 21:21:49,865 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 24 GetRequests, 17 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=55, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:49,865 INFO  L437           NwaCegarLoop]: 119 mSDtfsCounter, 9 mSDsluCounter, 62 mSDsCounter, 0 mSdLazyCounter, 201 mSolverCounterSat, 43 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 181 SdHoareTripleChecker+Invalid, 244 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 43 IncrementalHoareTripleChecker+Valid, 201 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,866 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 181 Invalid, 244 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [43 Valid, 201 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:49,866 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 119 states.
[2025-04-28 21:21:49,900 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 119 to 103.
[2025-04-28 21:21:49,900 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 103 states, 28 states have (on average 4.0) internal successors, (112), 77 states have internal predecessors, (112), 51 states have call successors, (51), 4 states have call predecessors, (51), 23 states have return successors, (314), 21 states have call predecessors, (314), 51 states have call successors, (314)
[2025-04-28 21:21:49,903 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 103 states to 103 states and 477 transitions.
[2025-04-28 21:21:49,903 INFO  L79                 Accepts]: Start accepts. Automaton has 103 states and 477 transitions. Word has length 17
[2025-04-28 21:21:49,904 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,904 INFO  L485      AbstractCegarLoop]: Abstraction has 103 states and 477 transitions.
[2025-04-28 21:21:49,904 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:49,904 INFO  L278                IsEmpty]: Start isEmpty. Operand 103 states and 477 transitions.
[2025-04-28 21:21:49,911 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:49,911 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,911 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:49,915 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:50,111 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-04-28 21:21:50,112 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,112 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,112 INFO  L85        PathProgramCache]: Analyzing trace with hash -1045619755, now seen corresponding path program 1 times
[2025-04-28 21:21:50,112 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,112 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [720092665]
[2025-04-28 21:21:50,112 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,112 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,123 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:50,137 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:50,137 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,138 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,189 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:50,190 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,190 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [720092665]
[2025-04-28 21:21:50,190 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [720092665] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,190 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,190 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,190 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [114867899]
[2025-04-28 21:21:50,190 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,190 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,190 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,191 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,191 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,191 INFO  L87              Difference]: Start difference. First operand 103 states and 477 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:50,578 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,578 INFO  L93              Difference]: Finished difference Result 116 states and 458 transitions.
[2025-04-28 21:21:50,579 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:50,579 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:50,579 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,585 INFO  L225             Difference]: With dead ends: 116
[2025-04-28 21:21:50,585 INFO  L226             Difference]: Without dead ends: 101
[2025-04-28 21:21:50,585 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:50,586 INFO  L437           NwaCegarLoop]: 95 mSDtfsCounter, 2 mSDsluCounter, 60 mSDsCounter, 0 mSdLazyCounter, 171 mSolverCounterSat, 52 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 155 SdHoareTripleChecker+Invalid, 223 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 52 IncrementalHoareTripleChecker+Valid, 171 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,586 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 155 Invalid, 223 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [52 Valid, 171 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:50,587 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-04-28 21:21:50,611 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 85.
[2025-04-28 21:21:50,611 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 85 states, 24 states have (on average 5.083333333333333) internal successors, (122), 63 states have internal predecessors, (122), 42 states have call successors, (42), 5 states have call predecessors, (42), 18 states have return successors, (156), 16 states have call predecessors, (156), 42 states have call successors, (156)
[2025-04-28 21:21:50,613 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 85 states to 85 states and 320 transitions.
[2025-04-28 21:21:50,613 INFO  L79                 Accepts]: Start accepts. Automaton has 85 states and 320 transitions. Word has length 17
[2025-04-28 21:21:50,614 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,614 INFO  L485      AbstractCegarLoop]: Abstraction has 85 states and 320 transitions.
[2025-04-28 21:21:50,614 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:50,614 INFO  L278                IsEmpty]: Start isEmpty. Operand 85 states and 320 transitions.
[2025-04-28 21:21:50,618 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:50,618 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,618 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:50,618 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:21:50,618 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,619 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,619 INFO  L85        PathProgramCache]: Analyzing trace with hash -1909835763, now seen corresponding path program 1 times
[2025-04-28 21:21:50,619 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,619 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [539595820]
[2025-04-28 21:21:50,619 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,619 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,624 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:50,628 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:50,628 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,628 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,662 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:50,662 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,663 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [539595820]
[2025-04-28 21:21:50,663 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [539595820] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,663 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,663 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,663 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1519418544]
[2025-04-28 21:21:50,663 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,663 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,663 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,664 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,664 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,664 INFO  L87              Difference]: Start difference. First operand 85 states and 320 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:51,287 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,287 INFO  L93              Difference]: Finished difference Result 152 states and 585 transitions.
[2025-04-28 21:21:51,287 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:51,287 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:51,287 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,292 INFO  L225             Difference]: With dead ends: 152
[2025-04-28 21:21:51,293 INFO  L226             Difference]: Without dead ends: 138
[2025-04-28 21:21:51,293 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:51,293 INFO  L437           NwaCegarLoop]: 89 mSDtfsCounter, 21 mSDsluCounter, 16 mSDsCounter, 0 mSdLazyCounter, 324 mSolverCounterSat, 74 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 63 SdHoareTripleChecker+Valid, 105 SdHoareTripleChecker+Invalid, 398 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 74 IncrementalHoareTripleChecker+Valid, 324 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,294 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [63 Valid, 105 Invalid, 398 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [74 Valid, 324 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:51,294 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 138 states.
[2025-04-28 21:21:51,317 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 138 to 120.
[2025-04-28 21:21:51,318 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 120 states, 36 states have (on average 5.75) internal successors, (207), 88 states have internal predecessors, (207), 58 states have call successors, (58), 10 states have call predecessors, (58), 25 states have return successors, (199), 23 states have call predecessors, (199), 58 states have call successors, (199)
[2025-04-28 21:21:51,320 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 120 states to 120 states and 464 transitions.
[2025-04-28 21:21:51,321 INFO  L79                 Accepts]: Start accepts. Automaton has 120 states and 464 transitions. Word has length 17
[2025-04-28 21:21:51,321 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,321 INFO  L485      AbstractCegarLoop]: Abstraction has 120 states and 464 transitions.
[2025-04-28 21:21:51,321 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:51,321 INFO  L278                IsEmpty]: Start isEmpty. Operand 120 states and 464 transitions.
[2025-04-28 21:21:51,326 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:51,326 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,326 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:51,326 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:21:51,326 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,327 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,327 INFO  L85        PathProgramCache]: Analyzing trace with hash -390081215, now seen corresponding path program 1 times
[2025-04-28 21:21:51,327 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,327 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1114559678]
[2025-04-28 21:21:51,327 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,327 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,331 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:51,335 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:51,335 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,335 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,371 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:51,371 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,371 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1114559678]
[2025-04-28 21:21:51,371 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1114559678] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,371 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,372 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:51,372 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1934785664]
[2025-04-28 21:21:51,372 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,374 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:51,374 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,374 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:51,375 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:51,375 INFO  L87              Difference]: Start difference. First operand 120 states and 464 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:51,763 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,763 INFO  L93              Difference]: Finished difference Result 134 states and 511 transitions.
[2025-04-28 21:21:51,764 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:51,764 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:51,764 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,768 INFO  L225             Difference]: With dead ends: 134
[2025-04-28 21:21:51,768 INFO  L226             Difference]: Without dead ends: 134
[2025-04-28 21:21:51,769 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:51,769 INFO  L437           NwaCegarLoop]: 124 mSDtfsCounter, 9 mSDsluCounter, 66 mSDsCounter, 0 mSdLazyCounter, 182 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 190 SdHoareTripleChecker+Invalid, 223 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 182 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,769 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 190 Invalid, 223 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 182 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:51,770 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 134 states.
[2025-04-28 21:21:51,790 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 134 to 118.
[2025-04-28 21:21:51,791 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 118 states, 35 states have (on average 5.885714285714286) internal successors, (206), 87 states have internal predecessors, (206), 58 states have call successors, (58), 10 states have call predecessors, (58), 24 states have return successors, (173), 22 states have call predecessors, (173), 58 states have call successors, (173)
[2025-04-28 21:21:51,793 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 118 states to 118 states and 437 transitions.
[2025-04-28 21:21:51,794 INFO  L79                 Accepts]: Start accepts. Automaton has 118 states and 437 transitions. Word has length 17
[2025-04-28 21:21:51,794 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,794 INFO  L485      AbstractCegarLoop]: Abstraction has 118 states and 437 transitions.
[2025-04-28 21:21:51,794 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:51,794 INFO  L278                IsEmpty]: Start isEmpty. Operand 118 states and 437 transitions.
[2025-04-28 21:21:51,798 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:51,798 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,799 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:51,799 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-04-28 21:21:51,799 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,799 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,799 INFO  L85        PathProgramCache]: Analyzing trace with hash -536982457, now seen corresponding path program 1 times
[2025-04-28 21:21:51,799 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,799 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [670161589]
[2025-04-28 21:21:51,800 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,800 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,804 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:51,811 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:51,811 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,812 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,867 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:51,867 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,867 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [670161589]
[2025-04-28 21:21:51,867 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [670161589] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:51,867 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:51,867 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:51,867 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [586558806]
[2025-04-28 21:21:51,868 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,868 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:51,868 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,868 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:51,868 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:51,868 INFO  L87              Difference]: Start difference. First operand 118 states and 437 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:52,242 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,242 INFO  L93              Difference]: Finished difference Result 126 states and 488 transitions.
[2025-04-28 21:21:52,242 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:52,243 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:52,243 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,246 INFO  L225             Difference]: With dead ends: 126
[2025-04-28 21:21:52,246 INFO  L226             Difference]: Without dead ends: 113
[2025-04-28 21:21:52,247 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:52,247 INFO  L437           NwaCegarLoop]: 131 mSDtfsCounter, 8 mSDsluCounter, 93 mSDsCounter, 0 mSdLazyCounter, 165 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 224 SdHoareTripleChecker+Invalid, 193 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 165 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,247 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 224 Invalid, 193 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 165 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:52,248 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-04-28 21:21:52,267 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 103.
[2025-04-28 21:21:52,268 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 103 states, 29 states have (on average 6.655172413793103) internal successors, (193), 77 states have internal predecessors, (193), 55 states have call successors, (55), 10 states have call predecessors, (55), 18 states have return successors, (136), 17 states have call predecessors, (136), 55 states have call successors, (136)
[2025-04-28 21:21:52,269 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 103 states to 103 states and 384 transitions.
[2025-04-28 21:21:52,270 INFO  L79                 Accepts]: Start accepts. Automaton has 103 states and 384 transitions. Word has length 17
[2025-04-28 21:21:52,270 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,270 INFO  L485      AbstractCegarLoop]: Abstraction has 103 states and 384 transitions.
[2025-04-28 21:21:52,270 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:52,270 INFO  L278                IsEmpty]: Start isEmpty. Operand 103 states and 384 transitions.
[2025-04-28 21:21:52,274 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:52,274 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,274 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:52,274 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-04-28 21:21:52,274 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,275 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,275 INFO  L85        PathProgramCache]: Analyzing trace with hash -637557709, now seen corresponding path program 1 times
[2025-04-28 21:21:52,275 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,275 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [173205915]
[2025-04-28 21:21:52,275 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,275 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,281 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:52,295 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:52,295 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,295 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,415 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:52,415 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,415 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [173205915]
[2025-04-28 21:21:52,415 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [173205915] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,415 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,416 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:52,416 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [920860897]
[2025-04-28 21:21:52,416 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,416 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:52,416 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,417 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:52,417 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:52,417 INFO  L87              Difference]: Start difference. First operand 103 states and 384 transitions. Second operand  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:53,038 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,038 INFO  L93              Difference]: Finished difference Result 137 states and 493 transitions.
[2025-04-28 21:21:53,039 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:53,039 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 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:53,039 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,043 INFO  L225             Difference]: With dead ends: 137
[2025-04-28 21:21:53,043 INFO  L226             Difference]: Without dead ends: 137
[2025-04-28 21:21:53,043 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=27, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:53,044 INFO  L437           NwaCegarLoop]: 73 mSDtfsCounter, 5 mSDsluCounter, 35 mSDsCounter, 0 mSdLazyCounter, 415 mSolverCounterSat, 29 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 61 SdHoareTripleChecker+Valid, 108 SdHoareTripleChecker+Invalid, 444 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 29 IncrementalHoareTripleChecker+Valid, 415 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,044 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [61 Valid, 108 Invalid, 444 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [29 Valid, 415 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:53,045 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 137 states.
[2025-04-28 21:21:53,074 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 137 to 105.
[2025-04-28 21:21:53,074 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 105 states, 30 states have (on average 6.466666666666667) internal successors, (194), 78 states have internal predecessors, (194), 55 states have call successors, (55), 10 states have call predecessors, (55), 19 states have return successors, (145), 18 states have call predecessors, (145), 55 states have call successors, (145)
[2025-04-28 21:21:53,076 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 105 states to 105 states and 394 transitions.
[2025-04-28 21:21:53,077 INFO  L79                 Accepts]: Start accepts. Automaton has 105 states and 394 transitions. Word has length 17
[2025-04-28 21:21:53,077 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,077 INFO  L485      AbstractCegarLoop]: Abstraction has 105 states and 394 transitions.
[2025-04-28 21:21:53,077 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:53,077 INFO  L278                IsEmpty]: Start isEmpty. Operand 105 states and 394 transitions.
[2025-04-28 21:21:53,081 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:53,081 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,081 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:53,081 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-04-28 21:21:53,082 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,082 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,082 INFO  L85        PathProgramCache]: Analyzing trace with hash -1801733547, now seen corresponding path program 1 times
[2025-04-28 21:21:53,083 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,083 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1811712553]
[2025-04-28 21:21:53,083 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,083 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,093 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:53,101 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:53,101 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,102 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,194 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:53,194 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,194 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1811712553]
[2025-04-28 21:21:53,194 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1811712553] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,194 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,194 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:53,194 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [385888622]
[2025-04-28 21:21:53,194 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,194 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:53,195 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,195 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:53,195 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:53,195 INFO  L87              Difference]: Start difference. First operand 105 states and 394 transitions. Second operand  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:53,614 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,614 INFO  L93              Difference]: Finished difference Result 135 states and 502 transitions.
[2025-04-28 21:21:53,615 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:53,615 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 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:53,615 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,619 INFO  L225             Difference]: With dead ends: 135
[2025-04-28 21:21:53,619 INFO  L226             Difference]: Without dead ends: 135
[2025-04-28 21:21:53,619 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 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:53,620 INFO  L437           NwaCegarLoop]: 75 mSDtfsCounter, 3 mSDsluCounter, 35 mSDsCounter, 0 mSdLazyCounter, 332 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 110 SdHoareTripleChecker+Invalid, 344 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 332 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,620 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 110 Invalid, 344 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 332 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:53,621 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 135 states.
[2025-04-28 21:21:53,639 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 135 to 111.
[2025-04-28 21:21:53,639 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 111 states, 33 states have (on average 5.96969696969697) internal successors, (197), 81 states have internal predecessors, (197), 55 states have call successors, (55), 10 states have call predecessors, (55), 22 states have return successors, (193), 21 states have call predecessors, (193), 55 states have call successors, (193)
[2025-04-28 21:21:53,642 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 111 states to 111 states and 445 transitions.
[2025-04-28 21:21:53,642 INFO  L79                 Accepts]: Start accepts. Automaton has 111 states and 445 transitions. Word has length 17
[2025-04-28 21:21:53,642 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,642 INFO  L485      AbstractCegarLoop]: Abstraction has 111 states and 445 transitions.
[2025-04-28 21:21:53,642 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:53,642 INFO  L278                IsEmpty]: Start isEmpty. Operand 111 states and 445 transitions.
[2025-04-28 21:21:53,646 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:53,646 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,646 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:53,646 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-04-28 21:21:53,647 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,647 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,647 INFO  L85        PathProgramCache]: Analyzing trace with hash -1219645628, now seen corresponding path program 1 times
[2025-04-28 21:21:53,647 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,647 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [398502612]
[2025-04-28 21:21:53,647 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,647 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,652 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:53,660 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:53,660 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,660 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,761 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:53,761 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,761 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [398502612]
[2025-04-28 21:21:53,761 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [398502612] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:53,761 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:53,762 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:53,762 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [364128559]
[2025-04-28 21:21:53,762 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,762 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:53,762 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,762 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:53,763 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:53,763 INFO  L87              Difference]: Start difference. First operand 111 states and 445 transitions. Second operand  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:54,333 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,333 INFO  L93              Difference]: Finished difference Result 133 states and 497 transitions.
[2025-04-28 21:21:54,337 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:54,337 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 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:54,337 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,341 INFO  L225             Difference]: With dead ends: 133
[2025-04-28 21:21:54,341 INFO  L226             Difference]: Without dead ends: 133
[2025-04-28 21:21:54,341 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=27, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:54,343 INFO  L437           NwaCegarLoop]: 78 mSDtfsCounter, 4 mSDsluCounter, 36 mSDsCounter, 0 mSdLazyCounter, 361 mSolverCounterSat, 32 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 33 SdHoareTripleChecker+Valid, 114 SdHoareTripleChecker+Invalid, 393 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 32 IncrementalHoareTripleChecker+Valid, 361 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,343 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [33 Valid, 114 Invalid, 393 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [32 Valid, 361 Invalid, 0 Unknown, 0 Unchecked, 0.5s Time]
[2025-04-28 21:21:54,343 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 133 states.
[2025-04-28 21:21:54,361 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 133 to 113.
[2025-04-28 21:21:54,362 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 113 states, 34 states have (on average 5.823529411764706) internal successors, (198), 82 states have internal predecessors, (198), 55 states have call successors, (55), 10 states have call predecessors, (55), 23 states have return successors, (195), 22 states have call predecessors, (195), 55 states have call successors, (195)
[2025-04-28 21:21:54,364 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 448 transitions.
[2025-04-28 21:21:54,364 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 448 transitions. Word has length 17
[2025-04-28 21:21:54,364 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,364 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 448 transitions.
[2025-04-28 21:21:54,364 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:54,364 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 448 transitions.
[2025-04-28 21:21:54,368 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:54,368 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,368 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:54,368 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-04-28 21:21:54,368 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,369 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,369 INFO  L85        PathProgramCache]: Analyzing trace with hash 673519371, now seen corresponding path program 1 times
[2025-04-28 21:21:54,369 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,369 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [97023646]
[2025-04-28 21:21:54,369 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,369 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,375 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:54,457 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:54,459 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,459 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,625 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:54,626 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,626 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [97023646]
[2025-04-28 21:21:54,626 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [97023646] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,626 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [527631950]
[2025-04-28 21:21:54,626 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,626 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,629 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,630 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:54,637 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,681 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:54,706 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:54,707 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,707 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,708 INFO  L256         TraceCheckSpWp]: Trace formula consists of 190 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,709 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,810 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:54,810 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:55,215 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:55,216 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [527631950] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:55,216 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:55,216 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 14
[2025-04-28 21:21:55,216 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [258856848]
[2025-04-28 21:21:55,216 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,216 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:55,216 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,217 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:55,217 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=145, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:55,217 INFO  L87              Difference]: Start difference. First operand 113 states and 448 transitions. Second operand  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:56,185 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,185 INFO  L93              Difference]: Finished difference Result 187 states and 617 transitions.
[2025-04-28 21:21:56,185 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:21:56,186 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10) Word has length 17
[2025-04-28 21:21:56,186 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,192 INFO  L225             Difference]: With dead ends: 187
[2025-04-28 21:21:56,192 INFO  L226             Difference]: Without dead ends: 187
[2025-04-28 21:21:56,192 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 46 GetRequests, 29 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 46 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=70, Invalid=272, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:56,193 INFO  L437           NwaCegarLoop]: 76 mSDtfsCounter, 14 mSDsluCounter, 180 mSDsCounter, 0 mSdLazyCounter, 918 mSolverCounterSat, 32 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 256 SdHoareTripleChecker+Invalid, 950 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 32 IncrementalHoareTripleChecker+Valid, 918 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,196 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 256 Invalid, 950 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [32 Valid, 918 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:56,197 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 187 states.
[2025-04-28 21:21:56,220 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 187 to 113.
[2025-04-28 21:21:56,221 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 113 states, 34 states have (on average 5.823529411764706) internal successors, (198), 82 states have internal predecessors, (198), 55 states have call successors, (55), 10 states have call predecessors, (55), 23 states have return successors, (195), 22 states have call predecessors, (195), 55 states have call successors, (195)
[2025-04-28 21:21:56,226 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 448 transitions.
[2025-04-28 21:21:56,226 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 448 transitions. Word has length 17
[2025-04-28 21:21:56,226 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,226 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 448 transitions.
[2025-04-28 21:21:56,226 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:56,226 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 448 transitions.
[2025-04-28 21:21:56,231 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:56,232 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,232 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:56,237 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:56,432 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable23
[2025-04-28 21:21:56,433 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,433 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,433 INFO  L85        PathProgramCache]: Analyzing trace with hash 73599711, now seen corresponding path program 1 times
[2025-04-28 21:21:56,433 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,433 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2032995389]
[2025-04-28 21:21:56,433 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,433 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,438 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:56,471 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:56,472 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,472 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,607 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:56,607 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,607 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2032995389]
[2025-04-28 21:21:56,607 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2032995389] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,607 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [24703723]
[2025-04-28 21:21:56,607 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,607 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,610 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,612 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:56,616 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,657 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:56,683 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:56,683 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,684 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,685 INFO  L256         TraceCheckSpWp]: Trace formula consists of 166 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,686 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,798 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:56,798 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:57,193 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:57,193 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [24703723] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:57,193 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:57,193 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 8] total 14
[2025-04-28 21:21:57,193 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1434850807]
[2025-04-28 21:21:57,193 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,194 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:57,194 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,194 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:57,194 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=145, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:57,194 INFO  L87              Difference]: Start difference. First operand 113 states and 448 transitions. Second operand  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:58,104 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,104 INFO  L93              Difference]: Finished difference Result 177 states and 585 transitions.
[2025-04-28 21:21:58,105 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:21:58,105 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10) Word has length 17
[2025-04-28 21:21:58,105 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,117 INFO  L225             Difference]: With dead ends: 177
[2025-04-28 21:21:58,117 INFO  L226             Difference]: Without dead ends: 177
[2025-04-28 21:21:58,117 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 47 GetRequests, 29 SyntacticMatches, 0 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 49 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=82, Invalid=298, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:58,118 INFO  L437           NwaCegarLoop]: 78 mSDtfsCounter, 12 mSDsluCounter, 290 mSDsCounter, 0 mSdLazyCounter, 941 mSolverCounterSat, 46 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 368 SdHoareTripleChecker+Invalid, 987 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 46 IncrementalHoareTripleChecker+Valid, 941 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,118 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 368 Invalid, 987 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [46 Valid, 941 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:58,119 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 177 states.
[2025-04-28 21:21:58,139 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 177 to 113.
[2025-04-28 21:21:58,139 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 113 states, 34 states have (on average 5.823529411764706) internal successors, (198), 82 states have internal predecessors, (198), 55 states have call successors, (55), 10 states have call predecessors, (55), 23 states have return successors, (195), 22 states have call predecessors, (195), 55 states have call successors, (195)
[2025-04-28 21:21:58,141 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 113 states to 113 states and 448 transitions.
[2025-04-28 21:21:58,142 INFO  L79                 Accepts]: Start accepts. Automaton has 113 states and 448 transitions. Word has length 17
[2025-04-28 21:21:58,142 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,142 INFO  L485      AbstractCegarLoop]: Abstraction has 113 states and 448 transitions.
[2025-04-28 21:21:58,142 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:58,142 INFO  L278                IsEmpty]: Start isEmpty. Operand 113 states and 448 transitions.
[2025-04-28 21:21:58,146 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:58,146 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,146 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:58,152 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:58,350 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable24
[2025-04-28 21:21:58,351 INFO  L403      AbstractCegarLoop]: === Iteration 25 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,351 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,351 INFO  L85        PathProgramCache]: Analyzing trace with hash -1090576127, now seen corresponding path program 1 times
[2025-04-28 21:21:58,351 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,352 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [441246294]
[2025-04-28 21:21:58,352 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,352 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,357 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:58,366 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:58,366 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,366 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,455 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:58,455 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,455 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [441246294]
[2025-04-28 21:21:58,455 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [441246294] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:58,456 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:58,456 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:58,456 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1549062428]
[2025-04-28 21:21:58,456 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,456 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:58,456 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,457 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:58,457 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:58,457 INFO  L87              Difference]: Start difference. First operand 113 states and 448 transitions. Second operand  has 5 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 5 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
