./chc-comp-wrapper.sh ../../../chc-comp25-benchmarks/ultimate/Lia-NonLinArrays/09_fmaxsym_000.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-05-07 17:25:40,247 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-05-07 17:25:40,284 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_483b0f8a-eacf-4bc6-9e62-c7011a62a744/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-05-07 17:25:40,288 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-05-07 17:25:40,288 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-05-07 17:25:40,301 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-05-07 17:25:40,301 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-05-07 17:25:40,302 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-05-07 17:25:40,302 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-05-07 17:25:40,302 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-05-07 17:25:40,302 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-05-07 17:25:40,302 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-05-07 17:25:40,302 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-05-07 17:25:40,302 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-05-07 17:25:40,302 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-05-07 17:25:40,302 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-05-07 17:25:40,302 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-05-07 17:25:40,302 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-05-07 17:25:40,303 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:40,303 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-05-07 17:25:40,303 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-05-07 17:25:40,303 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-05-07 17:25:40,303 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-05-07 17:25:40,303 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-05-07 17:25:40,303 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-05-07 17:25:40,303 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-05-07 17:25:40,303 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-05-07 17:25:40,482 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-05-07 17:25:40,490 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-05-07 17:25:40,492 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-05-07 17:25:40,493 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-05-07 17:25:40,493 INFO  L274        PluginConnector]: SmtParser initialized
[2025-05-07 17:25:40,494 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_483b0f8a-eacf-4bc6-9e62-c7011a62a744/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/ultimate/Lia-NonLinArrays/09_fmaxsym_000.smt2
[2025-05-07 17:25:40,495 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-05-07 17:25:40,497 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-05-07 17:25:40,819 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_483b0f8a-eacf-4bc6-9e62-c7011a62a744/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp25-benchmarks/ultimate/Lia-NonLinArrays/09_fmaxsym_000.smt2
[2025-05-07 17:25:40,821 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-05-07 17:25:40,822 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-05-07 17:25:40,823 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-05-07 17:25:40,823 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-05-07 17:25:40,823 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-05-07 17:25:40,825 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,855 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40 Unit
[2025-05-07 17:25:40,855 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-05-07 17:25:40,856 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-05-07 17:25:40,856 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-05-07 17:25:40,856 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-05-07 17:25:40,866 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,866 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,885 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,885 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,893 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,895 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,899 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,902 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,903 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,913 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-05-07 17:25:40,914 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-05-07 17:25:40,914 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-05-07 17:25:40,914 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-05-07 17:25:40,915 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (1/1) ...
[2025-05-07 17:25:40,917 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-05-07 17:25:40,929 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:40,939 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-05-07 17:25:40,941 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-05-07 17:25:40,950 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-05-07 17:25:40,950 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-05-07 17:25:40,950 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-05-07 17:25:40,950 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Inv given in one single declaration
[2025-05-07 17:25:40,950 INFO  L130     BoogieDeclarations]: Found specification of procedure Inv
[2025-05-07 17:25:40,950 INFO  L138     BoogieDeclarations]: Found implementation of procedure Inv
[2025-05-07 17:25:40,950 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-05-07 17:25:40,950 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-05-07 17:25:40,950 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-05-07 17:25:40,998 INFO  L234             CfgBuilder]: Building ICFG
[2025-05-07 17:25:40,999 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-05-07 17:25:41,354 INFO  L?                        ?]: Removed 11 outVars from TransFormulas that were not future-live.
[2025-05-07 17:25:41,354 INFO  L283             CfgBuilder]: Performing block encoding
[2025-05-07 17:25:41,369 INFO  L304             CfgBuilder]: Using library mode
[2025-05-07 17:25:41,369 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-05-07 17:25:41,370 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:41 BoogieIcfgContainer
[2025-05-07 17:25:41,370 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-05-07 17:25:41,372 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-05-07 17:25:41,373 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-05-07 17:25:41,376 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-05-07 17:25:41,376 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 07.05 05:25:40" (1/3) ...
[2025-05-07 17:25:41,377 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@35a2d37f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 07.05 05:25:41, skipping insertion in model container
[2025-05-07 17:25:41,377 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 07.05 05:25:40" (2/3) ...
[2025-05-07 17:25:41,377 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@35a2d37f and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 07.05 05:25:41, skipping insertion in model container
[2025-05-07 17:25:41,377 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 07.05 05:25:41" (3/3) ...
[2025-05-07 17:25:41,378 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-05-07 17:25:41,392 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-05-07 17:25:41,394 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 94 locations, 339 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-05-07 17:25:41,429 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-05-07 17:25:41,441 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;@1aa46123, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-05-07 17:25:41,441 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-05-07 17:25:41,445 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 94 states, 6 states have (on average 14.0) internal successors, (84), 84 states have internal predecessors, (84), 85 states have call successors, (85), 2 states have call predecessors, (85), 2 states have return successors, (85), 9 states have call predecessors, (85), 85 states have call successors, (85)
[2025-05-07 17:25:41,484 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 6
[2025-05-07 17:25:41,484 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:41,485 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1]
[2025-05-07 17:25:41,485 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:41,488 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:41,489 INFO  L85        PathProgramCache]: Analyzing trace with hash 568252621, now seen corresponding path program 1 times
[2025-05-07 17:25:41,494 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:41,495 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1196353354]
[2025-05-07 17:25:41,495 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:41,496 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:41,511 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 5 statements into 1 equivalence classes.
[2025-05-07 17:25:41,513 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 5 of 5 statements.
[2025-05-07 17:25:41,513 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:41,513 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:41,533 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:41,533 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:41,533 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1196353354]
[2025-05-07 17:25:41,534 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1196353354] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:41,534 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:41,536 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [2] imperfect sequences [] total 2
[2025-05-07 17:25:41,537 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [484840594]
[2025-05-07 17:25:41,537 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:41,540 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 2 states
[2025-05-07 17:25:41,540 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:41,564 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 2 interpolants.
[2025-05-07 17:25:41,565 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-05-07 17:25:41,567 INFO  L87              Difference]: Start difference. First operand  has 94 states, 6 states have (on average 14.0) internal successors, (84), 84 states have internal predecessors, (84), 85 states have call successors, (85), 2 states have call predecessors, (85), 2 states have return successors, (85), 9 states have call predecessors, (85), 85 states have call successors, (85) Second operand  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-05-07 17:25:41,595 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:41,595 INFO  L93              Difference]: Finished difference Result 92 states and 251 transitions.
[2025-05-07 17:25:41,596 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 2 states. 
[2025-05-07 17:25:41,597 INFO  L79                 Accepts]: Start accepts. Automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1) Word has length 5
[2025-05-07 17:25:41,597 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:41,607 INFO  L225             Difference]: With dead ends: 92
[2025-05-07 17:25:41,608 INFO  L226             Difference]: Without dead ends: 92
[2025-05-07 17:25:41,609 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 2 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 0 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=1, Invalid=1, Unknown=0, NotChecked=0, Total=2
[2025-05-07 17:25:41,611 INFO  L437           NwaCegarLoop]: 251 mSDtfsCounter, 0 mSDsluCounter, 0 mSDsCounter, 0 mSdLazyCounter, 0 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 0 SdHoareTripleChecker+Valid, 251 SdHoareTripleChecker+Invalid, 0 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 0 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:41,611 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [0 Valid, 251 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 0 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-05-07 17:25:41,630 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 92 states.
[2025-05-07 17:25:41,683 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 92 to 92.
[2025-05-07 17:25:41,684 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 5 states have (on average 16.2) internal successors, (81), 81 states have internal predecessors, (81), 85 states have call successors, (85), 2 states have call predecessors, (85), 2 states have return successors, (85), 9 states have call predecessors, (85), 85 states have call successors, (85)
[2025-05-07 17:25:41,694 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 251 transitions.
[2025-05-07 17:25:41,695 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 251 transitions. Word has length 5
[2025-05-07 17:25:41,695 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:41,695 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 251 transitions.
[2025-05-07 17:25:41,696 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 2 states, 2 states have (on average 1.5) internal successors, (3), 1 states have internal predecessors, (3), 1 states have call successors, (1), 1 states have call predecessors, (1), 1 states have return successors, (1), 1 states have call predecessors, (1), 1 states have call successors, (1)
[2025-05-07 17:25:41,696 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 251 transitions.
[2025-05-07 17:25:41,717 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-05-07 17:25:41,718 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:41,718 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:41,718 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-05-07 17:25:41,718 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:41,719 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:41,719 INFO  L85        PathProgramCache]: Analyzing trace with hash 1872292359, now seen corresponding path program 1 times
[2025-05-07 17:25:41,719 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:41,719 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1626966579]
[2025-05-07 17:25:41,719 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:41,719 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:41,726 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-05-07 17:25:41,742 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-05-07 17:25:41,742 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:41,742 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:41,809 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-05-07 17:25:41,809 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:41,810 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1626966579]
[2025-05-07 17:25:41,810 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1626966579] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:41,810 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:41,810 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:41,810 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [62685532]
[2025-05-07 17:25:41,810 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:41,811 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:41,811 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:41,812 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:41,812 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:41,812 INFO  L87              Difference]: Start difference. First operand 92 states and 251 transitions. Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-05-07 17:25:42,836 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:42,836 INFO  L93              Difference]: Finished difference Result 139 states and 468 transitions.
[2025-05-07 17:25:42,837 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:42,837 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-05-07 17:25:42,837 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:42,847 INFO  L225             Difference]: With dead ends: 139
[2025-05-07 17:25:42,847 INFO  L226             Difference]: Without dead ends: 139
[2025-05-07 17:25:42,847 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-05-07 17:25:42,848 INFO  L437           NwaCegarLoop]: 252 mSDtfsCounter, 39 mSDsluCounter, 292 mSDsCounter, 0 mSdLazyCounter, 461 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 49 SdHoareTripleChecker+Valid, 544 SdHoareTripleChecker+Invalid, 581 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 461 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:42,848 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [49 Valid, 544 Invalid, 581 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 461 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-05-07 17:25:42,849 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 139 states.
[2025-05-07 17:25:42,898 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 139 to 139.
[2025-05-07 17:25:42,899 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 139 states, 7 states have (on average 17.285714285714285) internal successors, (121), 120 states have internal predecessors, (121), 130 states have call successors, (130), 3 states have call predecessors, (130), 3 states have return successors, (217), 16 states have call predecessors, (217), 130 states have call successors, (217)
[2025-05-07 17:25:42,905 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 139 states to 139 states and 468 transitions.
[2025-05-07 17:25:42,905 INFO  L79                 Accepts]: Start accepts. Automaton has 139 states and 468 transitions. Word has length 9
[2025-05-07 17:25:42,906 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:42,906 INFO  L485      AbstractCegarLoop]: Abstraction has 139 states and 468 transitions.
[2025-05-07 17:25:42,906 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-05-07 17:25:42,906 INFO  L278                IsEmpty]: Start isEmpty. Operand 139 states and 468 transitions.
[2025-05-07 17:25:42,930 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-05-07 17:25:42,930 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:42,930 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:42,930 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-05-07 17:25:42,930 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:42,931 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:42,931 INFO  L85        PathProgramCache]: Analyzing trace with hash 1481607810, now seen corresponding path program 1 times
[2025-05-07 17:25:42,931 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:42,931 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [440015401]
[2025-05-07 17:25:42,931 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:42,931 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:42,935 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-05-07 17:25:42,942 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-05-07 17:25:42,942 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:42,942 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:42,989 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:42,989 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:42,989 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [440015401]
[2025-05-07 17:25:42,989 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [440015401] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:25:42,989 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [636349792]
[2025-05-07 17:25:42,989 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:42,989 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:42,991 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:25:42,993 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:25:42,994 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-05-07 17:25:43,033 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-05-07 17:25:43,053 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-05-07 17:25:43,054 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:43,054 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:43,056 INFO  L256         TraceCheckSpWp]: Trace formula consists of 178 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-05-07 17:25:43,062 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:25:43,102 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:43,102 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:25:43,191 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:43,191 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [636349792] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:25:43,191 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:25:43,191 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 5
[2025-05-07 17:25:43,191 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1492976291]
[2025-05-07 17:25:43,191 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:25:43,191 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-05-07 17:25:43,192 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:43,192 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-05-07 17:25:43,192 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-05-07 17:25:43,192 INFO  L87              Difference]: Start difference. First operand 139 states and 468 transitions. Second operand  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-05-07 17:25:45,842 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:45,843 INFO  L93              Difference]: Finished difference Result 365 states and 1869 transitions.
[2025-05-07 17:25:45,843 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:25:45,843 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-05-07 17:25:45,843 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:45,873 INFO  L225             Difference]: With dead ends: 365
[2025-05-07 17:25:45,873 INFO  L226             Difference]: Without dead ends: 365
[2025-05-07 17:25:45,873 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 30 GetRequests, 23 SyntacticMatches, 3 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:25:45,874 INFO  L437           NwaCegarLoop]: 480 mSDtfsCounter, 115 mSDsluCounter, 517 mSDsCounter, 0 mSdLazyCounter, 1326 mSolverCounterSat, 418 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 144 SdHoareTripleChecker+Valid, 997 SdHoareTripleChecker+Invalid, 1744 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 418 IncrementalHoareTripleChecker+Valid, 1326 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:45,874 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [144 Valid, 997 Invalid, 1744 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [418 Valid, 1326 Invalid, 0 Unknown, 0 Unchecked, 2.6s Time]
[2025-05-07 17:25:45,875 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 365 states.
[2025-05-07 17:25:45,979 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 365 to 271.
[2025-05-07 17:25:45,980 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 271 states, 11 states have (on average 21.727272727272727) internal successors, (239), 236 states have internal predecessors, (239), 258 states have call successors, (258), 5 states have call predecessors, (258), 5 states have return successors, (654), 30 states have call predecessors, (654), 258 states have call successors, (654)
[2025-05-07 17:25:45,987 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 271 states to 271 states and 1151 transitions.
[2025-05-07 17:25:45,987 INFO  L79                 Accepts]: Start accepts. Automaton has 271 states and 1151 transitions. Word has length 12
[2025-05-07 17:25:45,988 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:45,988 INFO  L485      AbstractCegarLoop]: Abstraction has 271 states and 1151 transitions.
[2025-05-07 17:25:45,988 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 4 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 2 states have call successors, (3)
[2025-05-07 17:25:45,988 INFO  L278                IsEmpty]: Start isEmpty. Operand 271 states and 1151 transitions.
[2025-05-07 17:25:46,006 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:46,007 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:46,007 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:46,010 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-05-07 17:25:46,208 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:25:46,209 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:46,213 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:46,214 INFO  L85        PathProgramCache]: Analyzing trace with hash 666011148, now seen corresponding path program 1 times
[2025-05-07 17:25:46,214 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:46,214 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [224234519]
[2025-05-07 17:25:46,214 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:46,215 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:46,227 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:46,238 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:46,238 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:46,239 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:46,350 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:46,350 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:46,350 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [224234519]
[2025-05-07 17:25:46,350 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [224234519] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:46,351 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:46,351 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:46,351 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [959329536]
[2025-05-07 17:25:46,351 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:46,351 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:46,352 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:46,352 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:46,352 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:46,353 INFO  L87              Difference]: Start difference. First operand 271 states and 1151 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:47,155 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:47,155 INFO  L93              Difference]: Finished difference Result 459 states and 2518 transitions.
[2025-05-07 17:25:47,155 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:47,155 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-05-07 17:25:47,156 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:47,196 INFO  L225             Difference]: With dead ends: 459
[2025-05-07 17:25:47,196 INFO  L226             Difference]: Without dead ends: 459
[2025-05-07 17:25:47,196 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-05-07 17:25:47,197 INFO  L437           NwaCegarLoop]: 339 mSDtfsCounter, 39 mSDsluCounter, 375 mSDsCounter, 0 mSdLazyCounter, 488 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 67 SdHoareTripleChecker+Valid, 714 SdHoareTripleChecker+Invalid, 608 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 488 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:47,197 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [67 Valid, 714 Invalid, 608 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 488 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:25:47,198 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 459 states.
[2025-05-07 17:25:47,373 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 459 to 459.
[2025-05-07 17:25:47,375 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 459 states, 19 states have (on average 23.105263157894736) internal successors, (439), 392 states have internal predecessors, (439), 438 states have call successors, (438), 9 states have call predecessors, (438), 9 states have return successors, (1641), 58 states have call predecessors, (1641), 438 states have call successors, (1641)
[2025-05-07 17:25:47,391 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 459 states to 459 states and 2518 transitions.
[2025-05-07 17:25:47,391 INFO  L79                 Accepts]: Start accepts. Automaton has 459 states and 2518 transitions. Word has length 13
[2025-05-07 17:25:47,391 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:47,391 INFO  L485      AbstractCegarLoop]: Abstraction has 459 states and 2518 transitions.
[2025-05-07 17:25:47,391 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:47,391 INFO  L278                IsEmpty]: Start isEmpty. Operand 459 states and 2518 transitions.
[2025-05-07 17:25:47,411 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:47,412 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:47,412 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:47,412 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-05-07 17:25:47,412 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:47,413 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:47,413 INFO  L85        PathProgramCache]: Analyzing trace with hash -1775271096, now seen corresponding path program 1 times
[2025-05-07 17:25:47,413 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:47,413 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2125962456]
[2025-05-07 17:25:47,413 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:47,413 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:47,416 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:47,418 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:47,418 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:47,418 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:47,441 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:47,441 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:47,441 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2125962456]
[2025-05-07 17:25:47,441 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2125962456] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:47,441 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:47,441 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:47,441 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1707614476]
[2025-05-07 17:25:47,441 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:47,442 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:47,442 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:47,442 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:47,442 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:47,442 INFO  L87              Difference]: Start difference. First operand 459 states and 2518 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:48,326 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:48,326 INFO  L93              Difference]: Finished difference Result 647 states and 4227 transitions.
[2025-05-07 17:25:48,327 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:48,327 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-05-07 17:25:48,327 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:48,396 INFO  L225             Difference]: With dead ends: 647
[2025-05-07 17:25:48,397 INFO  L226             Difference]: Without dead ends: 647
[2025-05-07 17:25:48,397 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-05-07 17:25:48,397 INFO  L437           NwaCegarLoop]: 339 mSDtfsCounter, 39 mSDsluCounter, 369 mSDsCounter, 0 mSdLazyCounter, 491 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 70 SdHoareTripleChecker+Valid, 708 SdHoareTripleChecker+Invalid, 611 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 491 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:48,397 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [70 Valid, 708 Invalid, 611 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 491 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:25:48,398 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 647 states.
[2025-05-07 17:25:48,733 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 647 to 647.
[2025-05-07 17:25:48,738 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 647 states, 27 states have (on average 23.88888888888889) internal successors, (645), 548 states have internal predecessors, (645), 618 states have call successors, (618), 13 states have call predecessors, (618), 13 states have return successors, (2964), 86 states have call predecessors, (2964), 618 states have call successors, (2964)
[2025-05-07 17:25:48,766 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 647 states to 647 states and 4227 transitions.
[2025-05-07 17:25:48,766 INFO  L79                 Accepts]: Start accepts. Automaton has 647 states and 4227 transitions. Word has length 13
[2025-05-07 17:25:48,767 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:48,767 INFO  L485      AbstractCegarLoop]: Abstraction has 647 states and 4227 transitions.
[2025-05-07 17:25:48,767 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:48,767 INFO  L278                IsEmpty]: Start isEmpty. Operand 647 states and 4227 transitions.
[2025-05-07 17:25:48,792 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:48,792 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:48,792 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:48,792 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-05-07 17:25:48,792 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:48,793 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:48,793 INFO  L85        PathProgramCache]: Analyzing trace with hash -1265824254, now seen corresponding path program 1 times
[2025-05-07 17:25:48,793 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:48,793 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1463233466]
[2025-05-07 17:25:48,793 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:48,793 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:48,797 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:48,800 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:48,800 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:48,800 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:48,825 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:48,825 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:48,825 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1463233466]
[2025-05-07 17:25:48,825 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1463233466] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:48,825 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:48,826 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:48,826 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [485000696]
[2025-05-07 17:25:48,826 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:48,826 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:48,826 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:48,826 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:48,827 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:48,827 INFO  L87              Difference]: Start difference. First operand 647 states and 4227 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:49,664 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:49,664 INFO  L93              Difference]: Finished difference Result 835 states and 6274 transitions.
[2025-05-07 17:25:49,665 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:49,665 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-05-07 17:25:49,665 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:49,762 INFO  L225             Difference]: With dead ends: 835
[2025-05-07 17:25:49,762 INFO  L226             Difference]: Without dead ends: 835
[2025-05-07 17:25:49,763 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-05-07 17:25:49,763 INFO  L437           NwaCegarLoop]: 339 mSDtfsCounter, 39 mSDsluCounter, 367 mSDsCounter, 0 mSdLazyCounter, 492 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 71 SdHoareTripleChecker+Valid, 706 SdHoareTripleChecker+Invalid, 612 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 492 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:49,763 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [71 Valid, 706 Invalid, 612 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 492 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:25:49,764 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 835 states.
[2025-05-07 17:25:50,260 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 835 to 835.
[2025-05-07 17:25:50,264 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 835 states, 35 states have (on average 24.37142857142857) internal successors, (853), 704 states have internal predecessors, (853), 798 states have call successors, (798), 17 states have call predecessors, (798), 17 states have return successors, (4623), 114 states have call predecessors, (4623), 798 states have call successors, (4623)
[2025-05-07 17:25:50,319 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 835 states to 835 states and 6274 transitions.
[2025-05-07 17:25:50,319 INFO  L79                 Accepts]: Start accepts. Automaton has 835 states and 6274 transitions. Word has length 13
[2025-05-07 17:25:50,319 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:50,319 INFO  L485      AbstractCegarLoop]: Abstraction has 835 states and 6274 transitions.
[2025-05-07 17:25:50,319 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:50,319 INFO  L278                IsEmpty]: Start isEmpty. Operand 835 states and 6274 transitions.
[2025-05-07 17:25:50,353 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:50,353 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:50,354 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:50,354 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-05-07 17:25:50,354 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:50,355 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:50,355 INFO  L85        PathProgramCache]: Analyzing trace with hash 2029194494, now seen corresponding path program 1 times
[2025-05-07 17:25:50,355 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:50,355 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1545289854]
[2025-05-07 17:25:50,355 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:50,355 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:50,361 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:50,365 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:50,365 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:50,365 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:50,399 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:50,399 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:50,399 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1545289854]
[2025-05-07 17:25:50,399 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1545289854] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:50,399 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:50,399 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:50,399 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1278885903]
[2025-05-07 17:25:50,399 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:50,399 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:50,400 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:50,400 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:50,400 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:50,400 INFO  L87              Difference]: Start difference. First operand 835 states and 6274 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-05-07 17:25:51,853 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:51,853 INFO  L93              Difference]: Finished difference Result 965 states and 12420 transitions.
[2025-05-07 17:25:51,854 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:25:51,854 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-05-07 17:25:51,854 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:52,121 INFO  L225             Difference]: With dead ends: 965
[2025-05-07 17:25:52,122 INFO  L226             Difference]: Without dead ends: 965
[2025-05-07 17:25:52,122 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-05-07 17:25:52,122 INFO  L437           NwaCegarLoop]: 263 mSDtfsCounter, 40 mSDsluCounter, 236 mSDsCounter, 0 mSdLazyCounter, 829 mSolverCounterSat, 91 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 57 SdHoareTripleChecker+Valid, 499 SdHoareTripleChecker+Invalid, 920 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 91 IncrementalHoareTripleChecker+Valid, 829 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:52,123 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [57 Valid, 499 Invalid, 920 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [91 Valid, 829 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-05-07 17:25:52,124 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 965 states.
[2025-05-07 17:25:53,315 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 965 to 929.
[2025-05-07 17:25:53,318 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 929 states, 39 states have (on average 23.923076923076923) internal successors, (933), 782 states have internal predecessors, (933), 888 states have call successors, (888), 19 states have call predecessors, (888), 19 states have return successors, (5291), 128 states have call predecessors, (5291), 888 states have call successors, (5291)
[2025-05-07 17:25:53,366 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 929 states to 929 states and 7112 transitions.
[2025-05-07 17:25:53,366 INFO  L79                 Accepts]: Start accepts. Automaton has 929 states and 7112 transitions. Word has length 13
[2025-05-07 17:25:53,366 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:53,366 INFO  L485      AbstractCegarLoop]: Abstraction has 929 states and 7112 transitions.
[2025-05-07 17:25:53,366 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-05-07 17:25:53,366 INFO  L278                IsEmpty]: Start isEmpty. Operand 929 states and 7112 transitions.
[2025-05-07 17:25:53,399 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:53,399 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:53,399 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:53,399 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-05-07 17:25:53,399 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:53,401 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:53,401 INFO  L85        PathProgramCache]: Analyzing trace with hash 1884546563, now seen corresponding path program 1 times
[2025-05-07 17:25:53,401 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:53,401 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1331386210]
[2025-05-07 17:25:53,401 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:53,401 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:53,404 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:53,406 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:53,406 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:53,406 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:53,426 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:53,426 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:53,426 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1331386210]
[2025-05-07 17:25:53,427 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1331386210] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:53,427 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:53,427 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:53,427 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2097453572]
[2025-05-07 17:25:53,427 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:53,427 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:53,427 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:53,428 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:53,428 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:53,428 INFO  L87              Difference]: Start difference. First operand 929 states and 7112 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:54,265 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:54,265 INFO  L93              Difference]: Finished difference Result 1117 states and 9543 transitions.
[2025-05-07 17:25:54,266 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:54,266 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-05-07 17:25:54,266 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:54,446 INFO  L225             Difference]: With dead ends: 1117
[2025-05-07 17:25:54,446 INFO  L226             Difference]: Without dead ends: 1117
[2025-05-07 17:25:54,446 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-05-07 17:25:54,447 INFO  L437           NwaCegarLoop]: 335 mSDtfsCounter, 39 mSDsluCounter, 358 mSDsCounter, 0 mSdLazyCounter, 492 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 76 SdHoareTripleChecker+Valid, 693 SdHoareTripleChecker+Invalid, 612 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 492 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:54,447 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [76 Valid, 693 Invalid, 612 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 492 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-05-07 17:25:54,448 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1117 states.
[2025-05-07 17:25:55,387 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1117 to 1117.
[2025-05-07 17:25:55,392 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1117 states, 47 states have (on average 24.361702127659573) internal successors, (1145), 938 states have internal predecessors, (1145), 1068 states have call successors, (1068), 23 states have call predecessors, (1068), 23 states have return successors, (7330), 156 states have call predecessors, (7330), 1068 states have call successors, (7330)
[2025-05-07 17:25:55,456 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1117 states to 1117 states and 9543 transitions.
[2025-05-07 17:25:55,457 INFO  L79                 Accepts]: Start accepts. Automaton has 1117 states and 9543 transitions. Word has length 13
[2025-05-07 17:25:55,457 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:55,457 INFO  L485      AbstractCegarLoop]: Abstraction has 1117 states and 9543 transitions.
[2025-05-07 17:25:55,457 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:55,457 INFO  L278                IsEmpty]: Start isEmpty. Operand 1117 states and 9543 transitions.
[2025-05-07 17:25:55,494 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:55,494 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:55,494 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:55,494 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-05-07 17:25:55,494 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:55,495 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:55,495 INFO  L85        PathProgramCache]: Analyzing trace with hash 1100056656, now seen corresponding path program 1 times
[2025-05-07 17:25:55,495 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:55,495 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1986110037]
[2025-05-07 17:25:55,495 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:55,495 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:55,498 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:55,500 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:55,500 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:55,500 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:55,519 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:55,519 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:55,519 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1986110037]
[2025-05-07 17:25:55,519 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1986110037] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:55,519 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:55,519 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:55,519 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1613124735]
[2025-05-07 17:25:55,519 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:55,520 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:55,520 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:55,520 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:55,520 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:55,520 INFO  L87              Difference]: Start difference. First operand 1117 states and 9543 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:56,369 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:56,369 INFO  L93              Difference]: Finished difference Result 1305 states and 12314 transitions.
[2025-05-07 17:25:56,370 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:56,370 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-05-07 17:25:56,370 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:56,641 INFO  L225             Difference]: With dead ends: 1305
[2025-05-07 17:25:56,642 INFO  L226             Difference]: Without dead ends: 1305
[2025-05-07 17:25:56,642 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-05-07 17:25:56,642 INFO  L437           NwaCegarLoop]: 335 mSDtfsCounter, 39 mSDsluCounter, 354 mSDsCounter, 0 mSdLazyCounter, 494 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 78 SdHoareTripleChecker+Valid, 689 SdHoareTripleChecker+Invalid, 614 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 494 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:56,642 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [78 Valid, 689 Invalid, 614 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 494 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-05-07 17:25:56,643 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1305 states.
[2025-05-07 17:25:57,777 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1305 to 1305.
[2025-05-07 17:25:57,782 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1305 states, 55 states have (on average 24.745454545454546) internal successors, (1361), 1094 states have internal predecessors, (1361), 1248 states have call successors, (1248), 27 states have call predecessors, (1248), 27 states have return successors, (9705), 184 states have call predecessors, (9705), 1248 states have call successors, (9705)
[2025-05-07 17:25:57,871 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1305 states to 1305 states and 12314 transitions.
[2025-05-07 17:25:57,871 INFO  L79                 Accepts]: Start accepts. Automaton has 1305 states and 12314 transitions. Word has length 13
[2025-05-07 17:25:57,872 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:25:57,872 INFO  L485      AbstractCegarLoop]: Abstraction has 1305 states and 12314 transitions.
[2025-05-07 17:25:57,872 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:57,872 INFO  L278                IsEmpty]: Start isEmpty. Operand 1305 states and 12314 transitions.
[2025-05-07 17:25:57,910 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:25:57,910 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:25:57,910 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:25:57,910 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-05-07 17:25:57,910 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:25:57,911 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:25:57,911 INFO  L85        PathProgramCache]: Analyzing trace with hash 119053244, now seen corresponding path program 1 times
[2025-05-07 17:25:57,911 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:25:57,911 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1898479081]
[2025-05-07 17:25:57,911 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:25:57,911 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:25:57,914 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:25:57,916 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:25:57,916 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:25:57,916 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:25:57,934 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:25:57,934 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:25:57,934 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1898479081]
[2025-05-07 17:25:57,934 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1898479081] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:25:57,935 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:25:57,935 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:25:57,935 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [789975372]
[2025-05-07 17:25:57,935 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:25:57,935 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:25:57,935 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:25:57,935 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:25:57,935 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:25:57,936 INFO  L87              Difference]: Start difference. First operand 1305 states and 12314 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:25:58,851 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:25:58,851 INFO  L93              Difference]: Finished difference Result 1493 states and 15429 transitions.
[2025-05-07 17:25:58,852 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:25:58,852 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-05-07 17:25:58,852 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:25:59,213 INFO  L225             Difference]: With dead ends: 1493
[2025-05-07 17:25:59,213 INFO  L226             Difference]: Without dead ends: 1493
[2025-05-07 17:25:59,213 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-05-07 17:25:59,213 INFO  L437           NwaCegarLoop]: 335 mSDtfsCounter, 39 mSDsluCounter, 346 mSDsCounter, 0 mSdLazyCounter, 498 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 82 SdHoareTripleChecker+Valid, 681 SdHoareTripleChecker+Invalid, 618 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 498 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-05-07 17:25:59,214 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [82 Valid, 681 Invalid, 618 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 498 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-05-07 17:25:59,215 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1493 states.
[2025-05-07 17:26:00,945 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1493 to 1493.
[2025-05-07 17:26:00,952 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1493 states, 63 states have (on average 25.158730158730158) internal successors, (1585), 1250 states have internal predecessors, (1585), 1428 states have call successors, (1428), 31 states have call predecessors, (1428), 31 states have return successors, (12416), 212 states have call predecessors, (12416), 1428 states have call successors, (12416)
[2025-05-07 17:26:01,093 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1493 states to 1493 states and 15429 transitions.
[2025-05-07 17:26:01,093 INFO  L79                 Accepts]: Start accepts. Automaton has 1493 states and 15429 transitions. Word has length 13
[2025-05-07 17:26:01,093 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:01,093 INFO  L485      AbstractCegarLoop]: Abstraction has 1493 states and 15429 transitions.
[2025-05-07 17:26:01,093 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:26:01,093 INFO  L278                IsEmpty]: Start isEmpty. Operand 1493 states and 15429 transitions.
[2025-05-07 17:26:01,150 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:26:01,150 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:01,150 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:01,150 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-05-07 17:26:01,150 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:01,151 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:01,152 INFO  L85        PathProgramCache]: Analyzing trace with hash -126197609, now seen corresponding path program 1 times
[2025-05-07 17:26:01,152 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:01,152 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [988860366]
[2025-05-07 17:26:01,152 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:01,152 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:01,154 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:26:01,157 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:26:01,157 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:01,157 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:01,182 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:26:01,182 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:01,182 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [988860366]
[2025-05-07 17:26:01,182 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [988860366] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:01,183 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:01,183 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:01,183 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1503137664]
[2025-05-07 17:26:01,183 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:01,183 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:01,183 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:01,183 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:01,183 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:01,184 INFO  L87              Difference]: Start difference. First operand 1493 states and 15429 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:26:02,053 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:02,053 INFO  L93              Difference]: Finished difference Result 1681 states and 18882 transitions.
[2025-05-07 17:26:02,053 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:02,054 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-05-07 17:26:02,054 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:02,593 INFO  L225             Difference]: With dead ends: 1681
[2025-05-07 17:26:02,593 INFO  L226             Difference]: Without dead ends: 1681
[2025-05-07 17:26:02,593 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-05-07 17:26:02,594 INFO  L437           NwaCegarLoop]: 335 mSDtfsCounter, 39 mSDsluCounter, 344 mSDsCounter, 0 mSdLazyCounter, 497 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 83 SdHoareTripleChecker+Valid, 679 SdHoareTripleChecker+Invalid, 617 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 497 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:02,594 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [83 Valid, 679 Invalid, 617 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 497 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-05-07 17:26:02,595 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1681 states.
[2025-05-07 17:26:04,699 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1681 to 1681.
[2025-05-07 17:26:04,707 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1681 states, 71 states have (on average 25.507042253521128) internal successors, (1811), 1406 states have internal predecessors, (1811), 1608 states have call successors, (1608), 35 states have call predecessors, (1608), 35 states have return successors, (15463), 240 states have call predecessors, (15463), 1608 states have call successors, (15463)
[2025-05-07 17:26:04,874 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1681 states to 1681 states and 18882 transitions.
[2025-05-07 17:26:04,875 INFO  L79                 Accepts]: Start accepts. Automaton has 1681 states and 18882 transitions. Word has length 13
[2025-05-07 17:26:04,875 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:04,875 INFO  L485      AbstractCegarLoop]: Abstraction has 1681 states and 18882 transitions.
[2025-05-07 17:26:04,875 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:26:04,876 INFO  L278                IsEmpty]: Start isEmpty. Operand 1681 states and 18882 transitions.
[2025-05-07 17:26:04,924 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:26:04,924 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:04,924 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:04,924 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-05-07 17:26:04,925 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:04,926 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:04,926 INFO  L85        PathProgramCache]: Analyzing trace with hash -1385372312, now seen corresponding path program 1 times
[2025-05-07 17:26:04,926 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:04,926 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [573479794]
[2025-05-07 17:26:04,926 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:04,926 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:04,928 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:26:04,930 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:26:04,930 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:04,931 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:04,947 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:26:04,947 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:04,947 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [573479794]
[2025-05-07 17:26:04,948 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [573479794] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:04,948 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:04,948 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:04,948 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [512007676]
[2025-05-07 17:26:04,948 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:04,948 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:04,948 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:04,948 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:04,948 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:04,949 INFO  L87              Difference]: Start difference. First operand 1681 states and 18882 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:26:05,854 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:05,854 INFO  L93              Difference]: Finished difference Result 1869 states and 22673 transitions.
[2025-05-07 17:26:05,854 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:05,855 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-05-07 17:26:05,855 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:06,576 INFO  L225             Difference]: With dead ends: 1869
[2025-05-07 17:26:06,576 INFO  L226             Difference]: Without dead ends: 1869
[2025-05-07 17:26:06,576 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-05-07 17:26:06,576 INFO  L437           NwaCegarLoop]: 339 mSDtfsCounter, 39 mSDsluCounter, 347 mSDsCounter, 0 mSdLazyCounter, 498 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 81 SdHoareTripleChecker+Valid, 686 SdHoareTripleChecker+Invalid, 618 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 498 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:06,577 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [81 Valid, 686 Invalid, 618 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 498 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-05-07 17:26:06,577 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1869 states.
[2025-05-07 17:26:09,294 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1869 to 1869.
[2025-05-07 17:26:09,302 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1869 states, 79 states have (on average 25.810126582278482) internal successors, (2039), 1562 states have internal predecessors, (2039), 1788 states have call successors, (1788), 39 states have call predecessors, (1788), 39 states have return successors, (18846), 268 states have call predecessors, (18846), 1788 states have call successors, (18846)
[2025-05-07 17:26:09,499 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1869 states to 1869 states and 22673 transitions.
[2025-05-07 17:26:09,500 INFO  L79                 Accepts]: Start accepts. Automaton has 1869 states and 22673 transitions. Word has length 13
[2025-05-07 17:26:09,500 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:09,500 INFO  L485      AbstractCegarLoop]: Abstraction has 1869 states and 22673 transitions.
[2025-05-07 17:26:09,500 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:26:09,500 INFO  L278                IsEmpty]: Start isEmpty. Operand 1869 states and 22673 transitions.
[2025-05-07 17:26:09,553 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-05-07 17:26:09,553 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:09,553 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:09,554 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-05-07 17:26:09,554 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:09,555 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:09,555 INFO  L85        PathProgramCache]: Analyzing trace with hash 1892265413, now seen corresponding path program 1 times
[2025-05-07 17:26:09,555 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:09,555 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1841966917]
[2025-05-07 17:26:09,555 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:09,555 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:09,558 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-05-07 17:26:09,560 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-05-07 17:26:09,560 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:09,560 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:09,575 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-05-07 17:26:09,575 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:09,575 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1841966917]
[2025-05-07 17:26:09,575 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1841966917] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:09,575 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:09,575 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:09,575 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [222839601]
[2025-05-07 17:26:09,575 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:09,576 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:09,576 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:09,576 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:09,576 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:09,576 INFO  L87              Difference]: Start difference. First operand 1869 states and 22673 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:26:10,402 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:10,403 INFO  L93              Difference]: Finished difference Result 2057 states and 26802 transitions.
[2025-05-07 17:26:10,403 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-05-07 17:26:10,403 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-05-07 17:26:10,403 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:11,349 INFO  L225             Difference]: With dead ends: 2057
[2025-05-07 17:26:11,349 INFO  L226             Difference]: Without dead ends: 2057
[2025-05-07 17:26:11,349 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-05-07 17:26:11,350 INFO  L437           NwaCegarLoop]: 335 mSDtfsCounter, 39 mSDsluCounter, 340 mSDsCounter, 0 mSdLazyCounter, 501 mSolverCounterSat, 120 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 85 SdHoareTripleChecker+Valid, 675 SdHoareTripleChecker+Invalid, 621 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 120 IncrementalHoareTripleChecker+Valid, 501 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:11,350 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [85 Valid, 675 Invalid, 621 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [120 Valid, 501 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-05-07 17:26:11,351 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 2057 states.
[2025-05-07 17:26:15,160 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 2057 to 2057.
[2025-05-07 17:26:15,168 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 2057 states, 87 states have (on average 26.080459770114942) internal successors, (2269), 1718 states have internal predecessors, (2269), 1968 states have call successors, (1968), 43 states have call predecessors, (1968), 43 states have return successors, (22565), 296 states have call predecessors, (22565), 1968 states have call successors, (22565)
[2025-05-07 17:26:15,417 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2057 states to 2057 states and 26802 transitions.
[2025-05-07 17:26:15,417 INFO  L79                 Accepts]: Start accepts. Automaton has 2057 states and 26802 transitions. Word has length 13
[2025-05-07 17:26:15,417 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:15,417 INFO  L485      AbstractCegarLoop]: Abstraction has 2057 states and 26802 transitions.
[2025-05-07 17:26:15,417 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-05-07 17:26:15,417 INFO  L278                IsEmpty]: Start isEmpty. Operand 2057 states and 26802 transitions.
[2025-05-07 17:26:15,535 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-05-07 17:26:15,535 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:15,535 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:15,535 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-05-07 17:26:15,535 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:15,536 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:15,536 INFO  L85        PathProgramCache]: Analyzing trace with hash -1262627433, now seen corresponding path program 1 times
[2025-05-07 17:26:15,536 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:15,537 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [216780736]
[2025-05-07 17:26:15,537 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:15,537 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:15,540 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-05-07 17:26:15,542 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-05-07 17:26:15,542 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:15,542 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:15,565 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:26:15,566 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:15,566 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [216780736]
[2025-05-07 17:26:15,566 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [216780736] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:26:15,566 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [307259462]
[2025-05-07 17:26:15,566 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:15,566 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:26:15,567 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:26:15,569 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:26:15,570 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-05-07 17:26:15,603 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-05-07 17:26:15,622 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-05-07 17:26:15,622 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:15,622 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:15,623 INFO  L256         TraceCheckSpWp]: Trace formula consists of 263 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-05-07 17:26:15,625 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:26:15,635 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:26:15,635 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:26:15,720 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 2 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:26:15,720 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [307259462] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:26:15,721 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:26:15,721 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-05-07 17:26:15,721 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [278776228]
[2025-05-07 17:26:15,721 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:26:15,721 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:26:15,721 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:15,721 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:26:15,722 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:26:15,722 INFO  L87              Difference]: Start difference. First operand 2057 states and 26802 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:26:24,133 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:24,133 INFO  L93              Difference]: Finished difference Result 2225 states and 68684 transitions.
[2025-05-07 17:26:24,134 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-05-07 17:26:24,134 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 16
[2025-05-07 17:26:24,134 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:26,284 INFO  L225             Difference]: With dead ends: 2225
[2025-05-07 17:26:26,284 INFO  L226             Difference]: Without dead ends: 2225
[2025-05-07 17:26:26,284 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 44 GetRequests, 31 SyntacticMatches, 2 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 19 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=54, Invalid=102, Unknown=0, NotChecked=0, Total=156
[2025-05-07 17:26:26,285 INFO  L437           NwaCegarLoop]: 486 mSDtfsCounter, 122 mSDsluCounter, 472 mSDsCounter, 0 mSdLazyCounter, 3169 mSolverCounterSat, 543 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 7.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 470 SdHoareTripleChecker+Valid, 958 SdHoareTripleChecker+Invalid, 3712 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 543 IncrementalHoareTripleChecker+Valid, 3169 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 7.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:26,285 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [470 Valid, 958 Invalid, 3712 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [543 Valid, 3169 Invalid, 0 Unknown, 0 Unchecked, 7.6s Time]
[2025-05-07 17:26:26,286 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 2225 states.
[2025-05-07 17:26:31,281 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 2225 to 1963.
[2025-05-07 17:26:31,288 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1963 states, 83 states have (on average 26.373493975903614) internal successors, (2189), 1640 states have internal predecessors, (2189), 1878 states have call successors, (1878), 41 states have call predecessors, (1878), 41 states have return successors, (20613), 282 states have call predecessors, (20613), 1878 states have call successors, (20613)
[2025-05-07 17:26:31,480 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1963 states to 1963 states and 24680 transitions.
[2025-05-07 17:26:31,480 INFO  L79                 Accepts]: Start accepts. Automaton has 1963 states and 24680 transitions. Word has length 16
[2025-05-07 17:26:31,480 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:31,480 INFO  L485      AbstractCegarLoop]: Abstraction has 1963 states and 24680 transitions.
[2025-05-07 17:26:31,480 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:26:31,480 INFO  L278                IsEmpty]: Start isEmpty. Operand 1963 states and 24680 transitions.
[2025-05-07 17:26:31,534 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-05-07 17:26:31,534 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:31,534 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:31,539 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-05-07 17:26:31,735 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable14
[2025-05-07 17:26:31,735 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:31,741 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:31,741 INFO  L85        PathProgramCache]: Analyzing trace with hash -1000508605, now seen corresponding path program 1 times
[2025-05-07 17:26:31,741 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:31,741 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1229303046]
[2025-05-07 17:26:31,741 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:31,741 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:31,746 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-05-07 17:26:31,749 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-05-07 17:26:31,749 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:31,749 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:31,772 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:26:31,772 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:31,772 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1229303046]
[2025-05-07 17:26:31,772 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1229303046] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:31,772 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:31,772 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:31,772 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [450194995]
[2025-05-07 17:26:31,772 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:31,773 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:31,773 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:31,773 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:31,773 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:31,773 INFO  L87              Difference]: Start difference. First operand 1963 states and 24680 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-05-07 17:26:33,892 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:33,892 INFO  L93              Difference]: Finished difference Result 2435 states and 57576 transitions.
[2025-05-07 17:26:33,892 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:26:33,892 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-05-07 17:26:33,892 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:36,046 INFO  L225             Difference]: With dead ends: 2435
[2025-05-07 17:26:36,046 INFO  L226             Difference]: Without dead ends: 2435
[2025-05-07 17:26:36,047 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-05-07 17:26:36,047 INFO  L437           NwaCegarLoop]: 260 mSDtfsCounter, 40 mSDsluCounter, 212 mSDsCounter, 0 mSdLazyCounter, 823 mSolverCounterSat, 131 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 87 SdHoareTripleChecker+Valid, 472 SdHoareTripleChecker+Invalid, 954 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 131 IncrementalHoareTripleChecker+Valid, 823 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:36,047 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [87 Valid, 472 Invalid, 954 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [131 Valid, 823 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-05-07 17:26:36,048 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 2435 states.
[2025-05-07 17:26:40,721 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 2435 to 2339.
[2025-05-07 17:26:40,731 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 2339 states, 99 states have (on average 22.272727272727273) internal successors, (2205), 1952 states have internal predecessors, (2205), 2238 states have call successors, (2238), 49 states have call predecessors, (2238), 49 states have return successors, (26543), 338 states have call predecessors, (26543), 2238 states have call successors, (26543)
[2025-05-07 17:26:40,980 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2339 states to 2339 states and 30986 transitions.
[2025-05-07 17:26:40,980 INFO  L79                 Accepts]: Start accepts. Automaton has 2339 states and 30986 transitions. Word has length 17
[2025-05-07 17:26:40,981 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:40,981 INFO  L485      AbstractCegarLoop]: Abstraction has 2339 states and 30986 transitions.
[2025-05-07 17:26:40,981 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-05-07 17:26:40,981 INFO  L278                IsEmpty]: Start isEmpty. Operand 2339 states and 30986 transitions.
[2025-05-07 17:26:41,059 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-05-07 17:26:41,059 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:41,059 INFO  L218           NwaCegarLoop]: trace histogram [3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:41,059 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-05-07 17:26:41,059 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:41,061 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:41,061 INFO  L85        PathProgramCache]: Analyzing trace with hash 706657604, now seen corresponding path program 1 times
[2025-05-07 17:26:41,061 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:41,061 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [493219852]
[2025-05-07 17:26:41,061 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:41,061 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:41,065 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-05-07 17:26:41,069 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-05-07 17:26:41,069 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:41,069 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:41,104 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-05-07 17:26:41,104 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:41,105 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [493219852]
[2025-05-07 17:26:41,105 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [493219852] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:41,105 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:41,105 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:41,105 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [947332337]
[2025-05-07 17:26:41,105 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:41,105 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:41,105 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:41,105 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:41,106 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:41,106 INFO  L87              Difference]: Start difference. First operand 2339 states and 30986 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-05-07 17:26:42,843 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:42,843 INFO  L93              Difference]: Finished difference Result 2631 states and 62560 transitions.
[2025-05-07 17:26:42,844 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:26:42,844 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-05-07 17:26:42,845 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:45,228 INFO  L225             Difference]: With dead ends: 2631
[2025-05-07 17:26:45,228 INFO  L226             Difference]: Without dead ends: 2631
[2025-05-07 17:26:45,228 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-05-07 17:26:45,229 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 40 mSDsluCounter, 196 mSDsCounter, 0 mSdLazyCounter, 826 mSolverCounterSat, 133 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 116 SdHoareTripleChecker+Valid, 458 SdHoareTripleChecker+Invalid, 959 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 133 IncrementalHoareTripleChecker+Valid, 826 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:45,229 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [116 Valid, 458 Invalid, 959 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [133 Valid, 826 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-05-07 17:26:45,230 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 2631 states.
[2025-05-07 17:26:50,609 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 2631 to 2527.
[2025-05-07 17:26:50,620 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 2527 states, 107 states have (on average 22.401869158878505) internal successors, (2397), 2108 states have internal predecessors, (2397), 2418 states have call successors, (2418), 53 states have call predecessors, (2418), 53 states have return successors, (28847), 366 states have call predecessors, (28847), 2418 states have call successors, (28847)
[2025-05-07 17:26:50,897 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2527 states to 2527 states and 33662 transitions.
[2025-05-07 17:26:50,898 INFO  L79                 Accepts]: Start accepts. Automaton has 2527 states and 33662 transitions. Word has length 17
[2025-05-07 17:26:50,898 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:26:50,898 INFO  L485      AbstractCegarLoop]: Abstraction has 2527 states and 33662 transitions.
[2025-05-07 17:26:50,898 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-05-07 17:26:50,898 INFO  L278                IsEmpty]: Start isEmpty. Operand 2527 states and 33662 transitions.
[2025-05-07 17:26:50,999 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-05-07 17:26:50,999 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:26:50,999 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:26:51,000 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-05-07 17:26:51,000 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:26:51,001 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:26:51,001 INFO  L85        PathProgramCache]: Analyzing trace with hash -1846110984, now seen corresponding path program 1 times
[2025-05-07 17:26:51,001 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:26:51,001 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1700529574]
[2025-05-07 17:26:51,001 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:26:51,001 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:26:51,005 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-05-07 17:26:51,007 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-05-07 17:26:51,007 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:26:51,007 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:26:51,031 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:26:51,031 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:26:51,031 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1700529574]
[2025-05-07 17:26:51,031 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1700529574] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:26:51,031 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:26:51,031 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:26:51,031 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [476967211]
[2025-05-07 17:26:51,031 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:26:51,032 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:26:51,032 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:26:51,032 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:26:51,032 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:26:51,032 INFO  L87              Difference]: Start difference. First operand 2527 states and 33662 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-05-07 17:26:52,678 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:26:52,678 INFO  L93              Difference]: Finished difference Result 2729 states and 64842 transitions.
[2025-05-07 17:26:52,678 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:26:52,678 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 19
[2025-05-07 17:26:52,679 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:26:54,936 INFO  L225             Difference]: With dead ends: 2729
[2025-05-07 17:26:54,936 INFO  L226             Difference]: Without dead ends: 2729
[2025-05-07 17:26:54,936 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-05-07 17:26:54,937 INFO  L437           NwaCegarLoop]: 337 mSDtfsCounter, 40 mSDsluCounter, 463 mSDsCounter, 0 mSdLazyCounter, 536 mSolverCounterSat, 89 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 57 SdHoareTripleChecker+Valid, 800 SdHoareTripleChecker+Invalid, 625 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 89 IncrementalHoareTripleChecker+Valid, 536 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-05-07 17:26:54,937 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [57 Valid, 800 Invalid, 625 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [89 Valid, 536 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-05-07 17:26:54,938 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 2729 states.
[2025-05-07 17:27:00,128 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 2729 to 2621.
[2025-05-07 17:27:00,138 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 2621 states, 111 states have (on average 22.315315315315317) internal successors, (2477), 2186 states have internal predecessors, (2477), 2508 states have call successors, (2508), 55 states have call predecessors, (2508), 55 states have return successors, (29902), 380 states have call predecessors, (29902), 2508 states have call successors, (29902)
[2025-05-07 17:27:00,434 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2621 states to 2621 states and 34887 transitions.
[2025-05-07 17:27:00,435 INFO  L79                 Accepts]: Start accepts. Automaton has 2621 states and 34887 transitions. Word has length 19
[2025-05-07 17:27:00,435 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:00,435 INFO  L485      AbstractCegarLoop]: Abstraction has 2621 states and 34887 transitions.
[2025-05-07 17:27:00,435 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-05-07 17:27:00,435 INFO  L278                IsEmpty]: Start isEmpty. Operand 2621 states and 34887 transitions.
[2025-05-07 17:27:00,555 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-05-07 17:27:00,555 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:00,555 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:00,556 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-05-07 17:27:00,556 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:00,556 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:00,556 INFO  L85        PathProgramCache]: Analyzing trace with hash -1925826599, now seen corresponding path program 1 times
[2025-05-07 17:27:00,556 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:00,556 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [580907264]
[2025-05-07 17:27:00,556 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:00,556 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:00,560 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-05-07 17:27:00,562 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-05-07 17:27:00,562 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:00,562 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:00,581 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:27:00,581 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:00,581 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [580907264]
[2025-05-07 17:27:00,582 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [580907264] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:00,582 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:00,582 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:00,582 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [343806023]
[2025-05-07 17:27:00,582 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:00,582 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:00,582 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:00,582 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:00,583 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:00,583 INFO  L87              Difference]: Start difference. First operand 2621 states and 34887 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:27:02,612 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:02,612 INFO  L93              Difference]: Finished difference Result 2925 states and 69380 transitions.
[2025-05-07 17:27:02,612 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:02,612 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-05-07 17:27:02,612 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:05,130 INFO  L225             Difference]: With dead ends: 2925
[2025-05-07 17:27:05,130 INFO  L226             Difference]: Without dead ends: 2925
[2025-05-07 17:27:05,131 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-05-07 17:27:05,131 INFO  L437           NwaCegarLoop]: 420 mSDtfsCounter, 39 mSDsluCounter, 339 mSDsCounter, 0 mSdLazyCounter, 390 mSolverCounterSat, 266 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 116 SdHoareTripleChecker+Valid, 759 SdHoareTripleChecker+Invalid, 656 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 266 IncrementalHoareTripleChecker+Valid, 390 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:05,131 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [116 Valid, 759 Invalid, 656 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [266 Valid, 390 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-05-07 17:27:05,134 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 2925 states.
[2025-05-07 17:27:11,447 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 2925 to 2809.
[2025-05-07 17:27:11,458 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 2809 states, 119 states have (on average 22.176470588235293) internal successors, (2639), 2342 states have internal predecessors, (2639), 2688 states have call successors, (2688), 59 states have call predecessors, (2688), 59 states have return successors, (31998), 408 states have call predecessors, (31998), 2688 states have call successors, (31998)
[2025-05-07 17:27:11,782 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2809 states to 2809 states and 37325 transitions.
[2025-05-07 17:27:11,782 INFO  L79                 Accepts]: Start accepts. Automaton has 2809 states and 37325 transitions. Word has length 21
[2025-05-07 17:27:11,782 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:11,782 INFO  L485      AbstractCegarLoop]: Abstraction has 2809 states and 37325 transitions.
[2025-05-07 17:27:11,782 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:27:11,782 INFO  L278                IsEmpty]: Start isEmpty. Operand 2809 states and 37325 transitions.
[2025-05-07 17:27:11,913 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-05-07 17:27:11,913 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:11,913 INFO  L218           NwaCegarLoop]: trace histogram [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:11,913 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-05-07 17:27:11,913 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:11,915 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:11,915 INFO  L85        PathProgramCache]: Analyzing trace with hash 1795367112, now seen corresponding path program 1 times
[2025-05-07 17:27:11,915 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:11,915 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [796593163]
[2025-05-07 17:27:11,915 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:11,915 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:11,919 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-05-07 17:27:11,922 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-05-07 17:27:11,922 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:11,922 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:11,940 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 10 proven. 0 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-05-07 17:27:11,940 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:11,940 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [796593163]
[2025-05-07 17:27:11,940 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [796593163] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:11,940 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:11,940 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:11,940 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1047061024]
[2025-05-07 17:27:11,940 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:11,941 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:11,941 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:11,941 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:11,941 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:11,941 INFO  L87              Difference]: Start difference. First operand 2809 states and 37325 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:27:13,934 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:13,934 INFO  L93              Difference]: Finished difference Result 3121 states and 75138 transitions.
[2025-05-07 17:27:13,935 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:13,935 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-05-07 17:27:13,935 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:16,785 INFO  L225             Difference]: With dead ends: 3121
[2025-05-07 17:27:16,785 INFO  L226             Difference]: Without dead ends: 3121
[2025-05-07 17:27:16,785 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-05-07 17:27:16,786 INFO  L437           NwaCegarLoop]: 264 mSDtfsCounter, 40 mSDsluCounter, 209 mSDsCounter, 0 mSdLazyCounter, 732 mSolverCounterSat, 140 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 124 SdHoareTripleChecker+Valid, 473 SdHoareTripleChecker+Invalid, 872 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 140 IncrementalHoareTripleChecker+Valid, 732 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:16,786 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [124 Valid, 473 Invalid, 872 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [140 Valid, 732 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-05-07 17:27:16,787 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 3121 states.
[2025-05-07 17:27:22,957 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 3121 to 2997.
[2025-05-07 17:27:22,964 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 2997 states, 127 states have (on average 22.165354330708663) internal successors, (2815), 2498 states have internal predecessors, (2815), 2868 states have call successors, (2868), 63 states have call predecessors, (2868), 63 states have return successors, (34697), 436 states have call predecessors, (34697), 2868 states have call successors, (34697)
[2025-05-07 17:27:23,305 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2997 states to 2997 states and 40380 transitions.
[2025-05-07 17:27:23,305 INFO  L79                 Accepts]: Start accepts. Automaton has 2997 states and 40380 transitions. Word has length 21
[2025-05-07 17:27:23,305 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:23,305 INFO  L485      AbstractCegarLoop]: Abstraction has 2997 states and 40380 transitions.
[2025-05-07 17:27:23,305 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:27:23,305 INFO  L278                IsEmpty]: Start isEmpty. Operand 2997 states and 40380 transitions.
[2025-05-07 17:27:23,446 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-05-07 17:27:23,446 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:23,446 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:23,446 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19
[2025-05-07 17:27:23,446 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:23,447 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:23,447 INFO  L85        PathProgramCache]: Analyzing trace with hash 1948958701, now seen corresponding path program 1 times
[2025-05-07 17:27:23,447 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:23,447 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2031965828]
[2025-05-07 17:27:23,447 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:23,447 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:23,451 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-05-07 17:27:23,453 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-05-07 17:27:23,453 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:23,453 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:23,468 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:27:23,468 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:23,468 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2031965828]
[2025-05-07 17:27:23,468 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2031965828] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:23,468 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:23,468 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:23,468 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [910558690]
[2025-05-07 17:27:23,468 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:23,468 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:23,468 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:23,469 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:23,469 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:23,469 INFO  L87              Difference]: Start difference. First operand 2997 states and 40380 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-05-07 17:27:24,966 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:24,966 INFO  L93              Difference]: Finished difference Result 3121 states and 74946 transitions.
[2025-05-07 17:27:24,967 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:24,967 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 19
[2025-05-07 17:27:24,967 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:27,862 INFO  L225             Difference]: With dead ends: 3121
[2025-05-07 17:27:27,862 INFO  L226             Difference]: Without dead ends: 3121
[2025-05-07 17:27:27,862 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-05-07 17:27:27,863 INFO  L437           NwaCegarLoop]: 382 mSDtfsCounter, 39 mSDsluCounter, 526 mSDsCounter, 0 mSdLazyCounter, 534 mSolverCounterSat, 85 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 47 SdHoareTripleChecker+Valid, 908 SdHoareTripleChecker+Invalid, 619 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 85 IncrementalHoareTripleChecker+Valid, 534 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:27,863 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [47 Valid, 908 Invalid, 619 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [85 Valid, 534 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-05-07 17:27:27,864 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 3121 states.
[2025-05-07 17:27:34,418 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 3121 to 2997.
[2025-05-07 17:27:34,430 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 2997 states, 127 states have (on average 22.165354330708663) internal successors, (2815), 2498 states have internal predecessors, (2815), 2868 states have call successors, (2868), 63 states have call predecessors, (2868), 63 states have return successors, (34601), 436 states have call predecessors, (34601), 2868 states have call successors, (34601)
[2025-05-07 17:27:34,782 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 2997 states to 2997 states and 40284 transitions.
[2025-05-07 17:27:34,782 INFO  L79                 Accepts]: Start accepts. Automaton has 2997 states and 40284 transitions. Word has length 19
[2025-05-07 17:27:34,782 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:34,782 INFO  L485      AbstractCegarLoop]: Abstraction has 2997 states and 40284 transitions.
[2025-05-07 17:27:34,782 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-05-07 17:27:34,782 INFO  L278                IsEmpty]: Start isEmpty. Operand 2997 states and 40284 transitions.
[2025-05-07 17:27:34,918 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 20
[2025-05-07 17:27:34,918 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:34,918 INFO  L218           NwaCegarLoop]: trace histogram [4, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:34,918 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-05-07 17:27:34,918 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:34,920 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:34,920 INFO  L85        PathProgramCache]: Analyzing trace with hash -1487849423, now seen corresponding path program 1 times
[2025-05-07 17:27:34,920 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:34,920 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1040179207]
[2025-05-07 17:27:34,920 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:34,920 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:34,923 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 19 statements into 1 equivalence classes.
[2025-05-07 17:27:34,924 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 19 of 19 statements.
[2025-05-07 17:27:34,924 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:34,925 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:34,939 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-05-07 17:27:34,939 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:34,939 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1040179207]
[2025-05-07 17:27:34,940 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1040179207] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:27:34,940 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:27:34,940 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:27:34,940 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [360762182]
[2025-05-07 17:27:34,940 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:27:34,940 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:27:34,940 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:34,940 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:27:34,940 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:27:34,940 INFO  L87              Difference]: Start difference. First operand 2997 states and 40284 transitions. Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-05-07 17:27:37,807 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:27:37,807 INFO  L93              Difference]: Finished difference Result 3955 states and 127881 transitions.
[2025-05-07 17:27:37,807 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:27:37,808 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4) Word has length 19
[2025-05-07 17:27:37,808 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:27:42,784 INFO  L225             Difference]: With dead ends: 3955
[2025-05-07 17:27:42,784 INFO  L226             Difference]: Without dead ends: 3955
[2025-05-07 17:27:42,784 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-05-07 17:27:42,785 INFO  L437           NwaCegarLoop]: 339 mSDtfsCounter, 41 mSDsluCounter, 312 mSDsCounter, 0 mSdLazyCounter, 799 mSolverCounterSat, 148 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 64 SdHoareTripleChecker+Valid, 651 SdHoareTripleChecker+Invalid, 947 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 148 IncrementalHoareTripleChecker+Valid, 799 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:27:42,785 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [64 Valid, 651 Invalid, 947 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [148 Valid, 799 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-05-07 17:27:42,786 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 3955 states.
[2025-05-07 17:27:55,932 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 3955 to 3815.
[2025-05-07 17:27:55,957 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 3815 states, 251 states have (on average 13.749003984063744) internal successors, (3451), 2820 states have internal predecessors, (3451), 3562 states have call successors, (3562), 125 states have call predecessors, (3562), 125 states have return successors, (81481), 870 states have call predecessors, (81481), 3562 states have call successors, (81481)
[2025-05-07 17:27:56,955 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 3815 states to 3815 states and 88494 transitions.
[2025-05-07 17:27:56,955 INFO  L79                 Accepts]: Start accepts. Automaton has 3815 states and 88494 transitions. Word has length 19
[2025-05-07 17:27:56,955 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:27:56,955 INFO  L485      AbstractCegarLoop]: Abstraction has 3815 states and 88494 transitions.
[2025-05-07 17:27:56,955 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (4), 1 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 2 states have call successors, (4)
[2025-05-07 17:27:56,955 INFO  L278                IsEmpty]: Start isEmpty. Operand 3815 states and 88494 transitions.
[2025-05-07 17:27:57,170 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 23
[2025-05-07 17:27:57,170 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:27:57,170 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:27:57,171 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-05-07 17:27:57,171 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:27:57,173 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:27:57,173 INFO  L85        PathProgramCache]: Analyzing trace with hash -1826270784, now seen corresponding path program 1 times
[2025-05-07 17:27:57,173 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:27:57,173 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [89819519]
[2025-05-07 17:27:57,173 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:57,173 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:27:57,176 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 22 statements into 1 equivalence classes.
[2025-05-07 17:27:57,179 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:27:57,179 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:57,179 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:57,207 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:27:57,207 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:27:57,207 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [89819519]
[2025-05-07 17:27:57,207 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [89819519] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:27:57,207 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1368178922]
[2025-05-07 17:27:57,207 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:27:57,207 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:27:57,209 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:27:57,211 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:27:57,212 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-05-07 17:27:57,255 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 22 statements into 1 equivalence classes.
[2025-05-07 17:27:57,294 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:27:57,294 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:27:57,294 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:27:57,295 INFO  L256         TraceCheckSpWp]: Trace formula consists of 432 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:27:57,297 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:27:57,309 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:27:57,309 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:27:57,447 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:27:57,447 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1368178922] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:27:57,447 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:27:57,447 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-05-07 17:27:57,447 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1643012375]
[2025-05-07 17:27:57,447 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:27:57,447 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:27:57,448 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:27:57,448 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:27:57,448 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:27:57,448 INFO  L87              Difference]: Start difference. First operand 3815 states and 88494 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:28:04,486 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:28:04,486 INFO  L93              Difference]: Finished difference Result 7666 states and 231433 transitions.
[2025-05-07 17:28:04,487 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:28:04,487 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 22
[2025-05-07 17:28:04,487 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:28:16,196 INFO  L225             Difference]: With dead ends: 7666
[2025-05-07 17:28:16,196 INFO  L226             Difference]: Without dead ends: 7666
[2025-05-07 17:28:16,196 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 51 GetRequests, 43 SyntacticMatches, 3 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:28:16,199 INFO  L437           NwaCegarLoop]: 574 mSDtfsCounter, 115 mSDsluCounter, 1147 mSDsCounter, 0 mSdLazyCounter, 2532 mSolverCounterSat, 284 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 132 SdHoareTripleChecker+Valid, 1721 SdHoareTripleChecker+Invalid, 2816 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 284 IncrementalHoareTripleChecker+Valid, 2532 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 3.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:28:16,199 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [132 Valid, 1721 Invalid, 2816 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [284 Valid, 2532 Invalid, 0 Unknown, 0 Unchecked, 3.2s Time]
[2025-05-07 17:28:16,203 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 7666 states.
[2025-05-07 17:28:47,497 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 7666 to 7489.
[2025-05-07 17:28:47,564 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 7489 states, 495 states have (on average 12.846464646464646) internal successors, (6359), 5518 states have internal predecessors, (6359), 6992 states have call successors, (6992), 247 states have call predecessors, (6992), 247 states have return successors, (210700), 1724 states have call predecessors, (210700), 6992 states have call successors, (210700)
[2025-05-07 17:28:51,127 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 7489 states to 7489 states and 224051 transitions.
[2025-05-07 17:28:51,127 INFO  L79                 Accepts]: Start accepts. Automaton has 7489 states and 224051 transitions. Word has length 22
[2025-05-07 17:28:51,128 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:28:51,128 INFO  L485      AbstractCegarLoop]: Abstraction has 7489 states and 224051 transitions.
[2025-05-07 17:28:51,128 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:28:51,128 INFO  L278                IsEmpty]: Start isEmpty. Operand 7489 states and 224051 transitions.
[2025-05-07 17:28:51,461 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 23
[2025-05-07 17:28:51,461 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:28:51,461 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:28:51,465 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-05-07 17:28:51,662 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:51,662 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:28:51,666 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:28:51,666 INFO  L85        PathProgramCache]: Analyzing trace with hash 1396823017, now seen corresponding path program 2 times
[2025-05-07 17:28:51,666 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:28:51,666 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1582627388]
[2025-05-07 17:28:51,667 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:28:51,667 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:28:51,685 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 22 statements into 2 equivalence classes.
[2025-05-07 17:28:51,695 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:28:51,695 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:28:51,695 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:51,723 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:28:51,723 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:28:51,723 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1582627388]
[2025-05-07 17:28:51,723 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1582627388] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:28:51,723 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [37697082]
[2025-05-07 17:28:51,723 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-05-07 17:28:51,724 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:28:51,726 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:28:51,728 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:28:51,728 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-05-07 17:28:51,773 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 22 statements into 2 equivalence classes.
[2025-05-07 17:28:51,818 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 22 of 22 statements.
[2025-05-07 17:28:51,818 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-05-07 17:28:51,818 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:28:51,819 INFO  L256         TraceCheckSpWp]: Trace formula consists of 433 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-05-07 17:28:51,820 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:28:51,834 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:28:51,834 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:28:51,987 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 4 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-05-07 17:28:51,987 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [37697082] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:28:51,987 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:28:51,987 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-05-07 17:28:51,988 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2120955548]
[2025-05-07 17:28:51,988 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:28:51,988 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:28:51,988 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:28:51,988 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:28:51,988 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:28:51,988 INFO  L87              Difference]: Start difference. First operand 7489 states and 224051 transitions. Second operand  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:29:03,538 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:29:03,538 INFO  L93              Difference]: Finished difference Result 11635 states and 472460 transitions.
[2025-05-07 17:29:03,538 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-05-07 17:29:03,538 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 22
[2025-05-07 17:29:03,538 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:29:37,686 INFO  L225             Difference]: With dead ends: 11635
[2025-05-07 17:29:37,686 INFO  L226             Difference]: Without dead ends: 11635
[2025-05-07 17:29:37,687 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 51 GetRequests, 43 SyntacticMatches, 3 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=28, Unknown=0, NotChecked=0, Total=42
[2025-05-07 17:29:37,687 INFO  L437           NwaCegarLoop]: 574 mSDtfsCounter, 115 mSDsluCounter, 1096 mSDsCounter, 0 mSdLazyCounter, 2580 mSolverCounterSat, 313 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 153 SdHoareTripleChecker+Valid, 1670 SdHoareTripleChecker+Invalid, 2893 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 313 IncrementalHoareTripleChecker+Valid, 2580 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 3.1s IncrementalHoareTripleChecker+Time
[2025-05-07 17:29:37,687 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [153 Valid, 1670 Invalid, 2893 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [313 Valid, 2580 Invalid, 0 Unknown, 0 Unchecked, 3.1s Time]
[2025-05-07 17:29:37,691 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 11635 states.
[2025-05-07 17:30:48,313 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 11635 to 11635.
[2025-05-07 17:30:48,461 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 11635 states, 771 states have (on average 12.87029831387808) internal successors, (9923), 8560 states have internal predecessors, (9923), 10862 states have call successors, (10862), 385 states have call predecessors, (10862), 385 states have return successors, (451675), 2690 states have call predecessors, (451675), 10862 states have call successors, (451675)
[2025-05-07 17:30:56,769 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 11635 states to 11635 states and 472460 transitions.
[2025-05-07 17:30:56,769 INFO  L79                 Accepts]: Start accepts. Automaton has 11635 states and 472460 transitions. Word has length 22
[2025-05-07 17:30:56,769 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:30:56,769 INFO  L485      AbstractCegarLoop]: Abstraction has 11635 states and 472460 transitions.
[2025-05-07 17:30:56,769 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-05-07 17:30:56,769 INFO  L278                IsEmpty]: Start isEmpty. Operand 11635 states and 472460 transitions.
[2025-05-07 17:30:57,223 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-05-07 17:30:57,223 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:30:57,223 INFO  L218           NwaCegarLoop]: trace histogram [5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:30:57,227 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-05-07 17:30:57,424 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable23
[2025-05-07 17:30:57,424 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:30:57,440 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:30:57,440 INFO  L85        PathProgramCache]: Analyzing trace with hash 1505819093, now seen corresponding path program 1 times
[2025-05-07 17:30:57,441 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:30:57,441 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [134671566]
[2025-05-07 17:30:57,441 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:30:57,441 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:30:57,458 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-05-07 17:30:57,465 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-05-07 17:30:57,466 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:30:57,466 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:30:57,503 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 2 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:30:57,503 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:30:57,503 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [134671566]
[2025-05-07 17:30:57,503 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [134671566] provided 0 perfect and 1 imperfect interpolant sequences
[2025-05-07 17:30:57,503 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [187551223]
[2025-05-07 17:30:57,503 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:30:57,504 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:30:57,506 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-05-07 17:30:57,508 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-05-07 17:30:57,509 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-05-07 17:30:57,553 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-05-07 17:30:57,579 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-05-07 17:30:57,579 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:30:57,579 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:30:57,580 INFO  L256         TraceCheckSpWp]: Trace formula consists of 441 conjuncts, 4 conjuncts are in the unsatisfiable core
[2025-05-07 17:30:57,582 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-05-07 17:30:57,591 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 2 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:30:57,591 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-05-07 17:30:57,720 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 2 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:30:57,720 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [187551223] provided 0 perfect and 2 imperfect interpolant sequences
[2025-05-07 17:30:57,720 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-05-07 17:30:57,720 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 5, 5] total 6
[2025-05-07 17:30:57,720 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [755662460]
[2025-05-07 17:30:57,720 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-05-07 17:30:57,721 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-05-07 17:30:57,721 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:30:57,721 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-05-07 17:30:57,721 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=10, Invalid=20, Unknown=0, NotChecked=0, Total=30
[2025-05-07 17:30:57,721 INFO  L87              Difference]: Start difference. First operand 11635 states and 472460 transitions. Second operand  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-05-07 17:31:18,338 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:31:18,338 INFO  L93              Difference]: Finished difference Result 12419 states and 924405 transitions.
[2025-05-07 17:31:18,339 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-05-07 17:31:18,339 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7) Word has length 24
[2025-05-07 17:31:18,339 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:32:24,315 INFO  L225             Difference]: With dead ends: 12419
[2025-05-07 17:32:24,315 INFO  L226             Difference]: Without dead ends: 12419
[2025-05-07 17:32:24,316 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 47 SyntacticMatches, 2 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=36, Invalid=74, Unknown=0, NotChecked=0, Total=110
[2025-05-07 17:32:24,316 INFO  L437           NwaCegarLoop]: 504 mSDtfsCounter, 120 mSDsluCounter, 930 mSDsCounter, 0 mSdLazyCounter, 3254 mSolverCounterSat, 359 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 4.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 162 SdHoareTripleChecker+Valid, 1434 SdHoareTripleChecker+Invalid, 3613 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 359 IncrementalHoareTripleChecker+Valid, 3254 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 4.6s IncrementalHoareTripleChecker+Time
[2025-05-07 17:32:24,316 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [162 Valid, 1434 Invalid, 3613 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [359 Valid, 3254 Invalid, 0 Unknown, 0 Unchecked, 4.6s Time]
[2025-05-07 17:32:24,320 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 12419 states.
[2025-05-07 17:35:15,675 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 12419 to 11635.
[2025-05-07 17:35:15,816 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 11635 states, 771 states have (on average 12.87029831387808) internal successors, (9923), 8560 states have internal predecessors, (9923), 10862 states have call successors, (10862), 385 states have call predecessors, (10862), 385 states have return successors, (447247), 2690 states have call predecessors, (447247), 10862 states have call successors, (447247)
[2025-05-07 17:35:24,822 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 11635 states to 11635 states and 468032 transitions.
[2025-05-07 17:35:24,822 INFO  L79                 Accepts]: Start accepts. Automaton has 11635 states and 468032 transitions. Word has length 24
[2025-05-07 17:35:24,822 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:35:24,822 INFO  L485      AbstractCegarLoop]: Abstraction has 11635 states and 468032 transitions.
[2025-05-07 17:35:24,822 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 2 states have call predecessors, (7), 3 states have call successors, (7)
[2025-05-07 17:35:24,822 INFO  L278                IsEmpty]: Start isEmpty. Operand 11635 states and 468032 transitions.
[2025-05-07 17:35:25,375 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-05-07 17:35:25,376 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:35:25,376 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:35:25,379 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-05-07 17:35:25,576 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable24,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-05-07 17:35:25,577 INFO  L403      AbstractCegarLoop]: === Iteration 25 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:35:25,578 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:35:25,578 INFO  L85        PathProgramCache]: Analyzing trace with hash -890754890, now seen corresponding path program 1 times
[2025-05-07 17:35:25,578 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:35:25,578 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [246846793]
[2025-05-07 17:35:25,578 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:35:25,578 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:35:25,591 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-05-07 17:35:25,595 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-05-07 17:35:25,595 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:35:25,595 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:35:25,623 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:35:25,623 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:35:25,623 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [246846793]
[2025-05-07 17:35:25,623 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [246846793] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:35:25,623 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:35:25,623 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:35:25,624 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1704939320]
[2025-05-07 17:35:25,624 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:35:25,624 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:35:25,624 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:35:25,624 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:35:25,624 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:35:25,624 INFO  L87              Difference]: Start difference. First operand 11635 states and 468032 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:35:53,408 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:35:53,408 INFO  L93              Difference]: Finished difference Result 14887 states and 1314779 transitions.
[2025-05-07 17:35:53,409 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:35:53,409 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 23
[2025-05-07 17:35:53,409 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:37:50,559 INFO  L225             Difference]: With dead ends: 14887
[2025-05-07 17:37:50,559 INFO  L226             Difference]: Without dead ends: 14887
[2025-05-07 17:37:50,560 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-05-07 17:37:50,560 INFO  L437           NwaCegarLoop]: 336 mSDtfsCounter, 41 mSDsluCounter, 255 mSDsCounter, 0 mSdLazyCounter, 796 mSolverCounterSat, 150 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 101 SdHoareTripleChecker+Valid, 591 SdHoareTripleChecker+Invalid, 946 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 150 IncrementalHoareTripleChecker+Valid, 796 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:37:50,560 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [101 Valid, 591 Invalid, 946 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [150 Valid, 796 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-05-07 17:37:50,564 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 14887 states.
[2025-05-07 17:41:37,506 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 14887 to 14087.
[2025-05-07 17:41:37,769 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 14087 states, 1155 states have (on average 13.96103896103896) internal successors, (16125), 9476 states have internal predecessors, (16125), 12930 states have call successors, (12930), 577 states have call predecessors, (12930), 577 states have return successors, (807129), 4034 states have call predecessors, (807129), 12930 states have call successors, (807129)
[2025-05-07 17:41:58,635 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 14087 states to 14087 states and 836184 transitions.
[2025-05-07 17:41:58,636 INFO  L79                 Accepts]: Start accepts. Automaton has 14087 states and 836184 transitions. Word has length 23
[2025-05-07 17:41:58,636 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-05-07 17:41:58,636 INFO  L485      AbstractCegarLoop]: Abstraction has 14087 states and 836184 transitions.
[2025-05-07 17:41:58,636 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:41:58,636 INFO  L278                IsEmpty]: Start isEmpty. Operand 14087 states and 836184 transitions.
[2025-05-07 17:41:59,579 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 24
[2025-05-07 17:41:59,579 INFO  L210           NwaCegarLoop]: Found error trace
[2025-05-07 17:41:59,579 INFO  L218           NwaCegarLoop]: trace histogram [5, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-05-07 17:41:59,579 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable25
[2025-05-07 17:41:59,579 INFO  L403      AbstractCegarLoop]: === Iteration 26 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-05-07 17:41:59,581 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-05-07 17:41:59,581 INFO  L85        PathProgramCache]: Analyzing trace with hash -1144953269, now seen corresponding path program 1 times
[2025-05-07 17:41:59,581 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-05-07 17:41:59,581 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1748559292]
[2025-05-07 17:41:59,581 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-05-07 17:41:59,581 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-05-07 17:41:59,585 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 23 statements into 1 equivalence classes.
[2025-05-07 17:41:59,588 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 23 of 23 statements.
[2025-05-07 17:41:59,588 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-05-07 17:41:59,588 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-05-07 17:41:59,605 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 14 proven. 0 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-05-07 17:41:59,606 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-05-07 17:41:59,606 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1748559292]
[2025-05-07 17:41:59,606 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1748559292] provided 1 perfect and 0 imperfect interpolant sequences
[2025-05-07 17:41:59,606 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-05-07 17:41:59,606 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-05-07 17:41:59,606 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [795725320]
[2025-05-07 17:41:59,606 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-05-07 17:41:59,606 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-05-07 17:41:59,606 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-05-07 17:41:59,607 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-05-07 17:41:59,607 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-05-07 17:41:59,607 INFO  L87              Difference]: Start difference. First operand 14087 states and 836184 transitions. Second operand  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-05-07 17:42:48,721 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-05-07 17:42:48,722 INFO  L93              Difference]: Finished difference Result 17371 states and 1893064 transitions.
[2025-05-07 17:42:48,722 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-05-07 17:42:48,722 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.0) internal successors, (9), 4 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 23
[2025-05-07 17:42:48,723 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-05-07 17:46:24,769 INFO  L225             Difference]: With dead ends: 17371
[2025-05-07 17:46:24,769 INFO  L226             Difference]: Without dead ends: 17371
[2025-05-07 17:46:24,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-05-07 17:46:24,769 INFO  L437           NwaCegarLoop]: 336 mSDtfsCounter, 41 mSDsluCounter, 249 mSDsCounter, 0 mSdLazyCounter, 794 mSolverCounterSat, 150 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 107 SdHoareTripleChecker+Valid, 585 SdHoareTripleChecker+Invalid, 944 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 150 IncrementalHoareTripleChecker+Valid, 794 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-05-07 17:46:24,770 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [107 Valid, 585 Invalid, 944 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [150 Valid, 794 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-05-07 17:46:24,773 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17371 states.
