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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:34,296 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:34,394 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f136edcf-2d2d-4891-bfd1-6d30abc7bcc2/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:34,399 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:34,400 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:34,431 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:34,432 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:34,432 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:34,434 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:34,434 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:34,434 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:34,435 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:34,435 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:34,435 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:34,435 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:34,436 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:34,437 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:34,437 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:34,437 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:34,437 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:34,437 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:34,437 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:34,437 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:34,437 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:34,437 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:34,439 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:34,439 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:34,768 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:34,780 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:34,783 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:34,786 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:34,787 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:34,788 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f136edcf-2d2d-4891-bfd1-6d30abc7bcc2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-121.smt2
[2025-04-28 21:21:34,790 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:34,796 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:34,932 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f136edcf-2d2d-4891-bfd1-6d30abc7bcc2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-121.smt2
[2025-04-28 21:21:34,935 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:34,938 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:34,938 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:34,939 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:34,939 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:34,943 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,964 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34 Unit
[2025-04-28 21:21:34,965 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:34,967 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:34,967 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:34,967 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:34,983 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:34,983 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,001 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,001 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,003 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,003 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,005 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,006 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,006 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,015 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:35,016 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:35,016 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:35,016 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:35,017 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,020 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:35,039 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,053 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:35,059 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:35,068 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:35,069 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:35,069 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:35,069 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure itp1 given in one single declaration
[2025-04-28 21:21:35,069 INFO  L130     BoogieDeclarations]: Found specification of procedure itp1
[2025-04-28 21:21:35,069 INFO  L138     BoogieDeclarations]: Found implementation of procedure itp1
[2025-04-28 21:21:35,069 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure itp given in one single declaration
[2025-04-28 21:21:35,070 INFO  L130     BoogieDeclarations]: Found specification of procedure itp
[2025-04-28 21:21:35,070 INFO  L138     BoogieDeclarations]: Found implementation of procedure itp
[2025-04-28 21:21:35,070 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:35,070 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:35,070 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:35,113 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:35,115 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:35,193 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:35,193 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:35,207 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:35,207 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:35,208 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:35 BoogieIcfgContainer
[2025-04-28 21:21:35,208 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:35,213 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:35,213 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:35,217 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:35,217 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:34" (1/3) ...
[2025-04-28 21:21:35,217 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@71767f08 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:35, skipping insertion in model container
[2025-04-28 21:21:35,218 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:34" (2/3) ...
[2025-04-28 21:21:35,218 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@71767f08 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:35, skipping insertion in model container
[2025-04-28 21:21:35,218 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:35" (3/3) ...
[2025-04-28 21:21:35,221 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:35,238 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:35,241 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 18 locations, 26 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:35,291 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:35,312 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;@db3883a, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:35,313 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:35,317 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 18 states, 8 states have (on average 1.375) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 3 states have return successors, (5), 4 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:35,325 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:35,325 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,326 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,327 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,332 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,333 INFO  L85        PathProgramCache]: Analyzing trace with hash -777061262, now seen corresponding path program 1 times
[2025-04-28 21:21:35,341 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,342 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [19581274]
[2025-04-28 21:21:35,342 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,343 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,376 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:35,400 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:35,400 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,400 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,512 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:35,513 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,513 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [19581274]
[2025-04-28 21:21:35,514 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [19581274] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,514 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:35,517 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:35,518 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1419123185]
[2025-04-28 21:21:35,519 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,522 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:35,523 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,551 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:35,552 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:35,554 INFO  L87              Difference]: Start difference. First operand  has 18 states, 8 states have (on average 1.375) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 3 states have return successors, (5), 4 states have call predecessors, (5), 5 states have call successors, (5) Second operand  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:35,619 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,620 INFO  L93              Difference]: Finished difference Result 20 states and 24 transitions.
[2025-04-28 21:21:35,621 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:35,623 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 13
[2025-04-28 21:21:35,623 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,629 INFO  L225             Difference]: With dead ends: 20
[2025-04-28 21:21:35,630 INFO  L226             Difference]: Without dead ends: 20
[2025-04-28 21:21:35,631 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:35,634 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 1 mSDsluCounter, 23 mSDsCounter, 0 mSdLazyCounter, 15 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 39 SdHoareTripleChecker+Invalid, 15 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 15 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,635 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 39 Invalid, 15 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 15 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:35,650 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 20 states.
[2025-04-28 21:21:35,698 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 20 to 18.
[2025-04-28 21:21:35,700 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 18 states, 8 states have (on average 1.25) internal successors, (10), 10 states have internal predecessors, (10), 5 states have call successors, (5), 3 states have call predecessors, (5), 4 states have return successors, (6), 4 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:35,703 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 18 states to 18 states and 21 transitions.
[2025-04-28 21:21:35,704 INFO  L79                 Accepts]: Start accepts. Automaton has 18 states and 21 transitions. Word has length 13
[2025-04-28 21:21:35,705 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,705 INFO  L485      AbstractCegarLoop]: Abstraction has 18 states and 21 transitions.
[2025-04-28 21:21:35,705 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.3333333333333335) internal successors, (7), 4 states have internal predecessors, (7), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:35,705 INFO  L278                IsEmpty]: Start isEmpty. Operand 18 states and 21 transitions.
[2025-04-28 21:21:35,706 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:35,707 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,707 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,707 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:35,707 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,708 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,708 INFO  L85        PathProgramCache]: Analyzing trace with hash 669490260, now seen corresponding path program 1 times
[2025-04-28 21:21:35,708 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,709 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1648572467]
[2025-04-28 21:21:35,709 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,709 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,715 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:35,733 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:35,734 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,735 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,913 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:35,916 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,917 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1648572467]
[2025-04-28 21:21:35,917 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1648572467] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:35,917 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [586127553]
[2025-04-28 21:21:35,917 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,917 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:35,920 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,927 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:35,929 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:35,974 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:36,000 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:36,000 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,000 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,002 INFO  L256         TraceCheckSpWp]: Trace formula consists of 52 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,006 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,167 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:36,167 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:36,167 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [586127553] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,167 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:36,167 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [6] total 9
[2025-04-28 21:21:36,169 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [52163187]
[2025-04-28 21:21:36,169 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,169 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:36,169 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,170 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:36,170 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=54, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:36,170 INFO  L87              Difference]: Start difference. First operand 18 states and 21 transitions. Second operand  has 5 states, 4 states have (on average 2.25) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:36,205 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,205 INFO  L93              Difference]: Finished difference Result 20 states and 23 transitions.
[2025-04-28 21:21:36,206 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:36,206 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 2.25) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4) Word has length 17
[2025-04-28 21:21:36,206 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,207 INFO  L225             Difference]: With dead ends: 20
[2025-04-28 21:21:36,207 INFO  L226             Difference]: Without dead ends: 20
[2025-04-28 21:21:36,207 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 22 GetRequests, 15 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=18, Invalid=54, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:36,210 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 1 mSDsluCounter, 34 mSDsCounter, 0 mSdLazyCounter, 18 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 50 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 18 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,210 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 50 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 18 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:36,211 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 20 states.
[2025-04-28 21:21:36,215 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 20 to 20.
[2025-04-28 21:21:36,215 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 20 states, 9 states have (on average 1.2222222222222223) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 5 states have return successors, (7), 5 states have call predecessors, (7), 5 states have call successors, (7)
[2025-04-28 21:21:36,216 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 23 transitions.
[2025-04-28 21:21:36,216 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 23 transitions. Word has length 17
[2025-04-28 21:21:36,216 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,216 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 23 transitions.
[2025-04-28 21:21:36,217 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 2.25) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:36,217 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 23 transitions.
[2025-04-28 21:21:36,219 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:36,220 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,220 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,226 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:36,421 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,421 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,422 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,423 INFO  L85        PathProgramCache]: Analyzing trace with hash -1739376522, now seen corresponding path program 1 times
[2025-04-28 21:21:36,423 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,423 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [407840955]
[2025-04-28 21:21:36,423 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,424 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,431 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:36,439 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:36,439 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,439 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,569 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:36,569 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,569 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [407840955]
[2025-04-28 21:21:36,570 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [407840955] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,570 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [203697555]
[2025-04-28 21:21:36,570 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,570 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,573 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,575 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:36,581 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,612 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:36,627 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:36,627 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,627 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,628 INFO  L256         TraceCheckSpWp]: Trace formula consists of 67 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,630 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,739 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:36,740 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:37,339 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:37,339 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [203697555] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:37,340 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:37,340 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 7, 7] total 13
[2025-04-28 21:21:37,340 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1741051115]
[2025-04-28 21:21:37,340 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,340 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:37,340 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,342 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:37,343 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=31, Invalid=125, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:37,343 INFO  L87              Difference]: Start difference. First operand 20 states and 23 transitions. Second operand  has 13 states, 7 states have (on average 3.0) internal successors, (21), 13 states have internal predecessors, (21), 8 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:37,582 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,583 INFO  L93              Difference]: Finished difference Result 30 states and 35 transitions.
[2025-04-28 21:21:37,583 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:37,583 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 7 states have (on average 3.0) internal successors, (21), 13 states have internal predecessors, (21), 8 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11) Word has length 21
[2025-04-28 21:21:37,584 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,584 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:37,584 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:37,585 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 36 SyntacticMatches, 3 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 35 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=65, Invalid=277, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:37,586 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 9 mSDsluCounter, 119 mSDsCounter, 0 mSdLazyCounter, 127 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 135 SdHoareTripleChecker+Invalid, 134 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 127 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,586 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 135 Invalid, 134 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 127 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:37,587 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:37,590 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 26.
[2025-04-28 21:21:37,590 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.25) internal successors, (15), 14 states have internal predecessors, (15), 6 states have call successors, (6), 4 states have call predecessors, (6), 7 states have return successors, (9), 7 states have call predecessors, (9), 6 states have call successors, (9)
[2025-04-28 21:21:37,591 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 30 transitions.
[2025-04-28 21:21:37,591 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 30 transitions. Word has length 21
[2025-04-28 21:21:37,591 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,592 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 30 transitions.
[2025-04-28 21:21:37,592 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 7 states have (on average 3.0) internal successors, (21), 13 states have internal predecessors, (21), 8 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:37,592 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 30 transitions.
[2025-04-28 21:21:37,593 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:37,593 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,593 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,598 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:37,797 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,797 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,797 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,797 INFO  L85        PathProgramCache]: Analyzing trace with hash 950748794, now seen corresponding path program 2 times
[2025-04-28 21:21:37,798 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,798 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [222819599]
[2025-04-28 21:21:37,798 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:37,798 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,804 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:37,818 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:37,818 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:37,818 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,936 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:37,936 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,936 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [222819599]
[2025-04-28 21:21:37,936 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [222819599] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,936 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [555005643]
[2025-04-28 21:21:37,936 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:37,936 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,939 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,941 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:37,944 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,983 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:38,000 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:38,000 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:38,000 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,001 INFO  L256         TraceCheckSpWp]: Trace formula consists of 97 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:38,003 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:38,118 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 4 proven. 7 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:38,119 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:39,008 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 4 proven. 8 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:39,009 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [555005643] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:39,009 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:39,009 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 8, 9] total 16
[2025-04-28 21:21:39,010 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1693388550]
[2025-04-28 21:21:39,010 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,010 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:39,010 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,011 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:39,011 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=194, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:39,011 INFO  L87              Difference]: Start difference. First operand 26 states and 30 transitions. Second operand  has 16 states, 9 states have (on average 2.7777777777777777) internal successors, (25), 16 states have internal predecessors, (25), 9 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (15), 8 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:21:39,234 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,234 INFO  L93              Difference]: Finished difference Result 34 states and 39 transitions.
[2025-04-28 21:21:39,236 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:39,237 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 9 states have (on average 2.7777777777777777) internal successors, (25), 16 states have internal predecessors, (25), 9 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (15), 8 states have call predecessors, (15), 9 states have call successors, (15) Word has length 29
[2025-04-28 21:21:39,237 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,238 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:39,238 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:39,238 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 74 GetRequests, 48 SyntacticMatches, 4 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 76 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=101, Invalid=451, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:39,239 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 14 mSDsluCounter, 100 mSDsCounter, 0 mSdLazyCounter, 90 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 116 SdHoareTripleChecker+Invalid, 102 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 90 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,239 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 116 Invalid, 102 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 90 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:39,240 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:39,245 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 30.
[2025-04-28 21:21:39,248 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 30 states, 14 states have (on average 1.2142857142857142) internal successors, (17), 16 states have internal predecessors, (17), 6 states have call successors, (6), 4 states have call predecessors, (6), 9 states have return successors, (11), 9 states have call predecessors, (11), 6 states have call successors, (11)
[2025-04-28 21:21:39,249 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 34 transitions.
[2025-04-28 21:21:39,250 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 34 transitions. Word has length 29
[2025-04-28 21:21:39,250 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,250 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 34 transitions.
[2025-04-28 21:21:39,251 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 9 states have (on average 2.7777777777777777) internal successors, (25), 16 states have internal predecessors, (25), 9 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (15), 8 states have call predecessors, (15), 9 states have call successors, (15)
[2025-04-28 21:21:39,251 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 34 transitions.
[2025-04-28 21:21:39,252 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:39,253 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,253 INFO  L218           NwaCegarLoop]: trace histogram [4, 4, 3, 3, 3, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,258 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:39,457 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,457 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,457 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,457 INFO  L85        PathProgramCache]: Analyzing trace with hash -1097980290, now seen corresponding path program 3 times
[2025-04-28 21:21:39,457 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,458 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [859821480]
[2025-04-28 21:21:39,458 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:39,458 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,464 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 37 statements into 4 equivalence classes.
[2025-04-28 21:21:39,477 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:39,477 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:39,477 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,652 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 6 proven. 14 refuted. 0 times theorem prover too weak. 22 trivial. 0 not checked.
[2025-04-28 21:21:39,653 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,653 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [859821480]
[2025-04-28 21:21:39,653 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [859821480] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,653 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1368334301]
[2025-04-28 21:21:39,653 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:39,653 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,656 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,658 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:39,661 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,699 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 37 statements into 4 equivalence classes.
[2025-04-28 21:21:39,721 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:39,721 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:39,721 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,722 INFO  L256         TraceCheckSpWp]: Trace formula consists of 127 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,726 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,770 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 6 proven. 14 refuted. 0 times theorem prover too weak. 22 trivial. 0 not checked.
[2025-04-28 21:21:39,770 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,992 INFO  L134       CoverageAnalysis]: Checked inductivity of 42 backedges. 6 proven. 17 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:40,993 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1368334301] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,993 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,993 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 11] total 13
[2025-04-28 21:21:40,993 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [644987664]
[2025-04-28 21:21:40,993 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,993 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:40,994 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,994 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:40,994 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=114, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:40,999 INFO  L87              Difference]: Start difference. First operand 30 states and 34 transitions. Second operand  has 13 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 13 states have internal predecessors, (18), 8 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (12), 7 states have call predecessors, (12), 8 states have call successors, (12)
[2025-04-28 21:21:41,107 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,108 INFO  L93              Difference]: Finished difference Result 36 states and 41 transitions.
[2025-04-28 21:21:41,110 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:41,111 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 13 states have internal predecessors, (18), 8 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (12), 7 states have call predecessors, (12), 8 states have call successors, (12) Word has length 37
[2025-04-28 21:21:41,111 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,112 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:41,114 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:41,115 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 87 GetRequests, 68 SyntacticMatches, 5 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 39 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=69, Invalid=171, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:41,116 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 5 mSDsluCounter, 75 mSDsCounter, 0 mSdLazyCounter, 57 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 91 SdHoareTripleChecker+Invalid, 58 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 57 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,116 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 91 Invalid, 58 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 57 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:41,116 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:41,120 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 32.
[2025-04-28 21:21:41,124 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 15 states have (on average 1.2) internal successors, (18), 17 states have internal predecessors, (18), 6 states have call successors, (6), 4 states have call predecessors, (6), 10 states have return successors, (12), 10 states have call predecessors, (12), 6 states have call successors, (12)
[2025-04-28 21:21:41,126 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 36 transitions.
[2025-04-28 21:21:41,126 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 36 transitions. Word has length 37
[2025-04-28 21:21:41,126 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,127 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 36 transitions.
[2025-04-28 21:21:41,127 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 13 states have internal predecessors, (18), 8 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (12), 7 states have call predecessors, (12), 8 states have call successors, (12)
[2025-04-28 21:21:41,127 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 36 transitions.
[2025-04-28 21:21:41,128 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:41,128 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,128 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,135 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:41,329 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:21:41,329 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,329 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,329 INFO  L85        PathProgramCache]: Analyzing trace with hash 1411039776, now seen corresponding path program 4 times
[2025-04-28 21:21:41,330 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,330 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [207769299]
[2025-04-28 21:21:41,330 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:41,330 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,336 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 41 statements into 2 equivalence classes.
[2025-04-28 21:21:41,345 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:41,345 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:41,345 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,636 INFO  L134       CoverageAnalysis]: Checked inductivity of 57 backedges. 0 proven. 14 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:41,636 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,636 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [207769299]
[2025-04-28 21:21:41,636 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [207769299] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,636 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [872178366]
[2025-04-28 21:21:41,636 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:41,636 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,639 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,641 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:41,644 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,696 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 41 statements into 2 equivalence classes.
[2025-04-28 21:21:41,718 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:21:41,718 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:41,718 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,719 INFO  L256         TraceCheckSpWp]: Trace formula consists of 142 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,720 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,869 INFO  L134       CoverageAnalysis]: Checked inductivity of 57 backedges. 6 proven. 22 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:21:41,869 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,559 INFO  L134       CoverageAnalysis]: Checked inductivity of 57 backedges. 6 proven. 28 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:43,559 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [872178366] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:43,560 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:43,560 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 10, 13] total 22
[2025-04-28 21:21:43,560 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [254383131]
[2025-04-28 21:21:43,560 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,563 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:43,563 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,566 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:43,567 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=81, Invalid=381, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:43,567 INFO  L87              Difference]: Start difference. First operand 32 states and 36 transitions. Second operand  has 22 states, 12 states have (on average 2.5833333333333335) internal successors, (31), 22 states have internal predecessors, (31), 12 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (20), 11 states have call predecessors, (20), 12 states have call successors, (20)
[2025-04-28 21:21:43,897 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,897 INFO  L93              Difference]: Finished difference Result 41 states and 47 transitions.
[2025-04-28 21:21:43,897 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:21:43,898 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 12 states have (on average 2.5833333333333335) internal successors, (31), 22 states have internal predecessors, (31), 12 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (20), 11 states have call predecessors, (20), 12 states have call successors, (20) Word has length 41
[2025-04-28 21:21:43,898 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,899 INFO  L225             Difference]: With dead ends: 41
[2025-04-28 21:21:43,899 INFO  L226             Difference]: Without dead ends: 39
[2025-04-28 21:21:43,899 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 103 GetRequests, 66 SyntacticMatches, 6 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 196 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=188, Invalid=868, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:43,900 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 20 mSDsluCounter, 145 mSDsCounter, 0 mSdLazyCounter, 161 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 28 SdHoareTripleChecker+Valid, 161 SdHoareTripleChecker+Invalid, 179 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 161 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,900 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [28 Valid, 161 Invalid, 179 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 161 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:43,901 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 39 states.
[2025-04-28 21:21:43,905 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 39 to 36.
[2025-04-28 21:21:43,905 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 17 states have (on average 1.1764705882352942) internal successors, (20), 19 states have internal predecessors, (20), 6 states have call successors, (6), 4 states have call predecessors, (6), 12 states have return successors, (14), 12 states have call predecessors, (14), 6 states have call successors, (14)
[2025-04-28 21:21:43,906 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 40 transitions.
[2025-04-28 21:21:43,906 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 40 transitions. Word has length 41
[2025-04-28 21:21:43,906 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,906 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 40 transitions.
[2025-04-28 21:21:43,907 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 12 states have (on average 2.5833333333333335) internal successors, (31), 22 states have internal predecessors, (31), 12 states have call successors, (16), 1 states have call predecessors, (16), 12 states have return successors, (20), 11 states have call predecessors, (20), 12 states have call successors, (20)
[2025-04-28 21:21:43,907 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 40 transitions.
[2025-04-28 21:21:43,908 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 50
[2025-04-28 21:21:43,908 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,908 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,912 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:44,112 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,112 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,112 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,112 INFO  L85        PathProgramCache]: Analyzing trace with hash -794953948, now seen corresponding path program 5 times
[2025-04-28 21:21:44,112 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,113 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [94970115]
[2025-04-28 21:21:44,113 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:44,113 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,125 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 49 statements into 6 equivalence classes.
[2025-04-28 21:21:44,145 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:21:44,146 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:44,146 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,376 INFO  L134       CoverageAnalysis]: Checked inductivity of 91 backedges. 8 proven. 33 refuted. 0 times theorem prover too weak. 50 trivial. 0 not checked.
[2025-04-28 21:21:44,376 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,376 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [94970115]
[2025-04-28 21:21:44,376 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [94970115] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:44,376 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2129830063]
[2025-04-28 21:21:44,377 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:44,377 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,379 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,381 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:44,385 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,456 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 49 statements into 6 equivalence classes.
[2025-04-28 21:21:44,490 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:21:44,490 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:44,490 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,491 INFO  L256         TraceCheckSpWp]: Trace formula consists of 172 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,493 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,727 INFO  L134       CoverageAnalysis]: Checked inductivity of 91 backedges. 0 proven. 50 refuted. 0 times theorem prover too weak. 41 trivial. 0 not checked.
[2025-04-28 21:21:44,727 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,298 INFO  L134       CoverageAnalysis]: Checked inductivity of 91 backedges. 0 proven. 66 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:51,299 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2129830063] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,299 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,299 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 16, 23] total 33
[2025-04-28 21:21:51,299 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1706351027]
[2025-04-28 21:21:51,299 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,300 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 33 states
[2025-04-28 21:21:51,300 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,301 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 33 interpolants.
[2025-04-28 21:21:51,301 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=188, Invalid=868, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:51,302 INFO  L87              Difference]: Start difference. First operand 36 states and 40 transitions. Second operand  has 33 states, 20 states have (on average 1.95) internal successors, (39), 33 states have internal predecessors, (39), 15 states have call successors, (17), 1 states have call predecessors, (17), 20 states have return successors, (31), 19 states have call predecessors, (31), 15 states have call successors, (31)
[2025-04-28 21:21:51,642 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,642 INFO  L93              Difference]: Finished difference Result 76 states and 82 transitions.
[2025-04-28 21:21:51,643 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 23 states. 
[2025-04-28 21:21:51,643 INFO  L79                 Accepts]: Start accepts. Automaton has  has 33 states, 20 states have (on average 1.95) internal successors, (39), 33 states have internal predecessors, (39), 15 states have call successors, (17), 1 states have call predecessors, (17), 20 states have return successors, (31), 19 states have call predecessors, (31), 15 states have call successors, (31) Word has length 49
[2025-04-28 21:21:51,644 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,644 INFO  L225             Difference]: With dead ends: 76
[2025-04-28 21:21:51,644 INFO  L226             Difference]: Without dead ends: 62
[2025-04-28 21:21:51,646 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 128 GetRequests, 70 SyntacticMatches, 11 SemanticMatches, 47 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 924 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=457, Invalid=1895, Unknown=0, NotChecked=0, Total=2352
[2025-04-28 21:21:51,647 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 29 mSDsluCounter, 177 mSDsCounter, 0 mSdLazyCounter, 144 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 39 SdHoareTripleChecker+Valid, 194 SdHoareTripleChecker+Invalid, 170 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 144 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,647 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [39 Valid, 194 Invalid, 170 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 144 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:51,648 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-04-28 21:21:51,654 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 52.
[2025-04-28 21:21:51,654 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 25 states have (on average 1.12) internal successors, (28), 27 states have internal predecessors, (28), 6 states have call successors, (6), 4 states have call predecessors, (6), 20 states have return successors, (23), 20 states have call predecessors, (23), 6 states have call successors, (23)
[2025-04-28 21:21:51,655 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 57 transitions.
[2025-04-28 21:21:51,655 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 57 transitions. Word has length 49
[2025-04-28 21:21:51,656 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,656 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 57 transitions.
[2025-04-28 21:21:51,656 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 33 states, 20 states have (on average 1.95) internal successors, (39), 33 states have internal predecessors, (39), 15 states have call successors, (17), 1 states have call predecessors, (17), 20 states have return successors, (31), 19 states have call predecessors, (31), 15 states have call successors, (31)
[2025-04-28 21:21:51,656 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 57 transitions.
[2025-04-28 21:21:51,657 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 58
[2025-04-28 21:21:51,657 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,657 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,664 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:51,862 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,862 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,862 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,862 INFO  L85        PathProgramCache]: Analyzing trace with hash -436634072, now seen corresponding path program 6 times
[2025-04-28 21:21:51,862 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,862 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [366923259]
[2025-04-28 21:21:51,862 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:51,862 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,870 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 57 statements into 7 equivalence classes.
[2025-04-28 21:21:51,882 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 57 of 57 statements.
[2025-04-28 21:21:51,882 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:51,883 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,102 INFO  L134       CoverageAnalysis]: Checked inductivity of 133 backedges. 13 proven. 48 refuted. 0 times theorem prover too weak. 72 trivial. 0 not checked.
[2025-04-28 21:21:52,102 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,102 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [366923259]
[2025-04-28 21:21:52,102 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [366923259] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,102 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [590377892]
[2025-04-28 21:21:52,102 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:52,102 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,105 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,107 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,111 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,272 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 57 statements into 7 equivalence classes.
[2025-04-28 21:21:52,302 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 57 of 57 statements.
[2025-04-28 21:21:52,302 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:52,302 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,303 INFO  L256         TraceCheckSpWp]: Trace formula consists of 202 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,305 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,455 INFO  L134       CoverageAnalysis]: Checked inductivity of 133 backedges. 0 proven. 30 refuted. 0 times theorem prover too weak. 103 trivial. 0 not checked.
[2025-04-28 21:21:52,456 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,009 INFO  L134       CoverageAnalysis]: Checked inductivity of 133 backedges. 0 proven. 40 refuted. 0 times theorem prover too weak. 93 trivial. 0 not checked.
[2025-04-28 21:21:56,009 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [590377892] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,009 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,009 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 10, 14] total 27
[2025-04-28 21:21:56,009 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [305005601]
[2025-04-28 21:21:56,009 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,009 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:21:56,010 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,010 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:21:56,011 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=120, Invalid=582, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:56,011 INFO  L87              Difference]: Start difference. First operand 52 states and 57 transitions. Second operand  has 27 states, 16 states have (on average 2.25) internal successors, (36), 27 states have internal predecessors, (36), 13 states have call successors, (17), 1 states have call predecessors, (17), 16 states have return successors, (25), 15 states have call predecessors, (25), 13 states have call successors, (25)
[2025-04-28 21:21:56,356 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,356 INFO  L93              Difference]: Finished difference Result 50 states and 64 transitions.
[2025-04-28 21:21:56,357 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 22 states. 
[2025-04-28 21:21:56,357 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 16 states have (on average 2.25) internal successors, (36), 27 states have internal predecessors, (36), 13 states have call successors, (17), 1 states have call predecessors, (17), 16 states have return successors, (25), 15 states have call predecessors, (25), 13 states have call successors, (25) Word has length 57
[2025-04-28 21:21:56,357 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,359 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:21:56,359 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:56,360 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 146 GetRequests, 100 SyntacticMatches, 6 SemanticMatches, 40 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 416 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=311, Invalid=1411, Unknown=0, NotChecked=0, Total=1722
[2025-04-28 21:21:56,364 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 34 mSDsluCounter, 122 mSDsCounter, 0 mSdLazyCounter, 150 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 44 SdHoareTripleChecker+Valid, 137 SdHoareTripleChecker+Invalid, 191 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 150 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,365 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [44 Valid, 137 Invalid, 191 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 150 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,365 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:56,377 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 46.
[2025-04-28 21:21:56,377 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 22 states have (on average 1.1818181818181819) internal successors, (26), 24 states have internal predecessors, (26), 7 states have call successors, (7), 5 states have call predecessors, (7), 16 states have return successors, (20), 16 states have call predecessors, (20), 7 states have call successors, (20)
[2025-04-28 21:21:56,378 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 53 transitions.
[2025-04-28 21:21:56,379 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 53 transitions. Word has length 57
[2025-04-28 21:21:56,380 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,380 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 53 transitions.
[2025-04-28 21:21:56,380 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 16 states have (on average 2.25) internal successors, (36), 27 states have internal predecessors, (36), 13 states have call successors, (17), 1 states have call predecessors, (17), 16 states have return successors, (25), 15 states have call predecessors, (25), 13 states have call successors, (25)
[2025-04-28 21:21:56,380 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 53 transitions.
[2025-04-28 21:21:56,382 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-04-28 21:21:56,382 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,382 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,387 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:56,587 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable8
[2025-04-28 21:21:56,587 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,587 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,587 INFO  L85        PathProgramCache]: Analyzing trace with hash 151279404, now seen corresponding path program 7 times
[2025-04-28 21:21:56,587 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,587 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2112980514]
[2025-04-28 21:21:56,587 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:56,587 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,594 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-04-28 21:21:56,608 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:21:56,608 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,608 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,800 INFO  L134       CoverageAnalysis]: Checked inductivity of 183 backedges. 0 proven. 42 refuted. 0 times theorem prover too weak. 141 trivial. 0 not checked.
[2025-04-28 21:21:56,801 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,801 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2112980514]
[2025-04-28 21:21:56,801 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2112980514] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,801 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1662657220]
[2025-04-28 21:21:56,801 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:56,801 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,804 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,806 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:56,809 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,998 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-04-28 21:21:57,027 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:21:57,027 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,027 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,029 INFO  L256         TraceCheckSpWp]: Trace formula consists of 232 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,030 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,246 INFO  L134       CoverageAnalysis]: Checked inductivity of 183 backedges. 12 proven. 61 refuted. 0 times theorem prover too weak. 110 trivial. 0 not checked.
[2025-04-28 21:21:57,246 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,541 INFO  L134       CoverageAnalysis]: Checked inductivity of 183 backedges. 12 proven. 82 refuted. 0 times theorem prover too weak. 89 trivial. 0 not checked.
[2025-04-28 21:22:01,542 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1662657220] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,542 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,542 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 13, 19] total 30
[2025-04-28 21:22:01,542 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1653479184]
[2025-04-28 21:22:01,542 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,542 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-04-28 21:22:01,543 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,543 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-04-28 21:22:01,544 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=156, Invalid=714, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:22:01,544 INFO  L87              Difference]: Start difference. First operand 46 states and 53 transitions. Second operand  has 30 states, 18 states have (on average 2.1666666666666665) internal successors, (39), 30 states have internal predecessors, (39), 14 states have call successors, (18), 1 states have call predecessors, (18), 18 states have return successors, (29), 17 states have call predecessors, (29), 14 states have call successors, (29)
[2025-04-28 21:22:01,932 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,932 INFO  L93              Difference]: Finished difference Result 54 states and 64 transitions.
[2025-04-28 21:22:01,932 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 23 states. 
[2025-04-28 21:22:01,932 INFO  L79                 Accepts]: Start accepts. Automaton has  has 30 states, 18 states have (on average 2.1666666666666665) internal successors, (39), 30 states have internal predecessors, (39), 14 states have call successors, (18), 1 states have call predecessors, (18), 18 states have return successors, (29), 17 states have call predecessors, (29), 14 states have call successors, (29) Word has length 65
[2025-04-28 21:22:01,933 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,934 INFO  L225             Difference]: With dead ends: 54
[2025-04-28 21:22:01,934 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:22:01,935 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 163 GetRequests, 109 SyntacticMatches, 9 SemanticMatches, 45 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 459 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=388, Invalid=1774, Unknown=0, NotChecked=0, Total=2162
[2025-04-28 21:22:01,935 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 55 mSDsluCounter, 139 mSDsCounter, 0 mSdLazyCounter, 128 mSolverCounterSat, 58 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 66 SdHoareTripleChecker+Valid, 155 SdHoareTripleChecker+Invalid, 186 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 58 IncrementalHoareTripleChecker+Valid, 128 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,936 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [66 Valid, 155 Invalid, 186 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [58 Valid, 128 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:01,940 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:22:01,947 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 50.
[2025-04-28 21:22:01,952 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 24 states have (on average 1.1666666666666667) internal successors, (28), 26 states have internal predecessors, (28), 7 states have call successors, (7), 5 states have call predecessors, (7), 18 states have return successors, (22), 18 states have call predecessors, (22), 7 states have call successors, (22)
[2025-04-28 21:22:01,952 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 57 transitions.
[2025-04-28 21:22:01,952 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 57 transitions. Word has length 65
[2025-04-28 21:22:01,953 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,953 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 57 transitions.
[2025-04-28 21:22:01,953 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 30 states, 18 states have (on average 2.1666666666666665) internal successors, (39), 30 states have internal predecessors, (39), 14 states have call successors, (18), 1 states have call predecessors, (18), 18 states have return successors, (29), 17 states have call predecessors, (29), 14 states have call successors, (29)
[2025-04-28 21:22:01,953 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 57 transitions.
[2025-04-28 21:22:01,954 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 74
[2025-04-28 21:22:01,954 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,955 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,960 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:22:02,158 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:22:02,158 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,158 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,158 INFO  L85        PathProgramCache]: Analyzing trace with hash -925531600, now seen corresponding path program 8 times
[2025-04-28 21:22:02,158 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,158 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1540235781]
[2025-04-28 21:22:02,158 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:02,159 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,166 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 73 statements into 2 equivalence classes.
[2025-04-28 21:22:02,181 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 73 of 73 statements.
[2025-04-28 21:22:02,181 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:02,181 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,402 INFO  L134       CoverageAnalysis]: Checked inductivity of 241 backedges. 0 proven. 56 refuted. 0 times theorem prover too weak. 185 trivial. 0 not checked.
[2025-04-28 21:22:02,402 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,402 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1540235781]
[2025-04-28 21:22:02,403 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1540235781] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,403 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1643569054]
[2025-04-28 21:22:02,403 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:02,403 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,405 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:02,408 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:02,411 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,651 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 73 statements into 2 equivalence classes.
[2025-04-28 21:22:02,684 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 73 of 73 statements.
[2025-04-28 21:22:02,684 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:02,685 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,686 INFO  L256         TraceCheckSpWp]: Trace formula consists of 262 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,688 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,888 INFO  L134       CoverageAnalysis]: Checked inductivity of 241 backedges. 14 proven. 78 refuted. 0 times theorem prover too weak. 149 trivial. 0 not checked.
[2025-04-28 21:22:02,889 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:08,467 INFO  L134       CoverageAnalysis]: Checked inductivity of 241 backedges. 14 proven. 106 refuted. 0 times theorem prover too weak. 121 trivial. 0 not checked.
[2025-04-28 21:22:08,467 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1643569054] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:08,467 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:08,467 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 14, 21] total 33
[2025-04-28 21:22:08,467 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [116178984]
[2025-04-28 21:22:08,467 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:08,468 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 33 states
[2025-04-28 21:22:08,468 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:08,468 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 33 interpolants.
[2025-04-28 21:22:08,469 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=188, Invalid=868, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:08,469 INFO  L87              Difference]: Start difference. First operand 50 states and 57 transitions. Second operand  has 33 states, 20 states have (on average 2.1) internal successors, (42), 33 states have internal predecessors, (42), 15 states have call successors, (19), 1 states have call predecessors, (19), 20 states have return successors, (32), 19 states have call predecessors, (32), 15 states have call successors, (32)
[2025-04-28 21:22:08,941 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:08,941 INFO  L93              Difference]: Finished difference Result 58 states and 68 transitions.
[2025-04-28 21:22:08,941 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 25 states. 
[2025-04-28 21:22:08,942 INFO  L79                 Accepts]: Start accepts. Automaton has  has 33 states, 20 states have (on average 2.1) internal successors, (42), 33 states have internal predecessors, (42), 15 states have call successors, (19), 1 states have call predecessors, (19), 20 states have return successors, (32), 19 states have call predecessors, (32), 15 states have call successors, (32) Word has length 73
[2025-04-28 21:22:08,943 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,943 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:22:08,946 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:22:08,947 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 183 GetRequests, 123 SyntacticMatches, 10 SemanticMatches, 50 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 583 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=475, Invalid=2177, Unknown=0, NotChecked=0, Total=2652
[2025-04-28 21:22:08,948 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 33 mSDsluCounter, 174 mSDsCounter, 0 mSdLazyCounter, 157 mSolverCounterSat, 28 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 45 SdHoareTripleChecker+Valid, 190 SdHoareTripleChecker+Invalid, 185 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 28 IncrementalHoareTripleChecker+Valid, 157 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,948 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [45 Valid, 190 Invalid, 185 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [28 Valid, 157 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:08,949 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:22:08,955 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 54.
[2025-04-28 21:22:08,956 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 54 states, 26 states have (on average 1.1538461538461537) internal successors, (30), 28 states have internal predecessors, (30), 7 states have call successors, (7), 5 states have call predecessors, (7), 20 states have return successors, (24), 20 states have call predecessors, (24), 7 states have call successors, (24)
[2025-04-28 21:22:08,956 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 61 transitions.
[2025-04-28 21:22:08,956 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 61 transitions. Word has length 73
[2025-04-28 21:22:08,957 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:08,957 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 61 transitions.
[2025-04-28 21:22:08,957 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 33 states, 20 states have (on average 2.1) internal successors, (42), 33 states have internal predecessors, (42), 15 states have call successors, (19), 1 states have call predecessors, (19), 20 states have return successors, (32), 19 states have call predecessors, (32), 15 states have call successors, (32)
[2025-04-28 21:22:08,957 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 61 transitions.
[2025-04-28 21:22:08,958 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 82
[2025-04-28 21:22:08,959 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:08,959 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:08,966 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:22:09,159 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable10
[2025-04-28 21:22:09,160 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,160 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,160 INFO  L85        PathProgramCache]: Analyzing trace with hash 1858338612, now seen corresponding path program 9 times
[2025-04-28 21:22:09,160 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,160 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1499446301]
[2025-04-28 21:22:09,160 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:09,160 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,173 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 81 statements into 10 equivalence classes.
[2025-04-28 21:22:09,202 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s) and asserted 77 of 81 statements.
[2025-04-28 21:22:09,202 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s)
[2025-04-28 21:22:09,202 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,515 INFO  L134       CoverageAnalysis]: Checked inductivity of 307 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 235 trivial. 0 not checked.
[2025-04-28 21:22:09,515 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:09,515 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1499446301]
[2025-04-28 21:22:09,515 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1499446301] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:09,516 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [442082081]
[2025-04-28 21:22:09,516 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:09,516 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:09,518 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:09,521 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:09,524 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:09,827 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 81 statements into 10 equivalence classes.
[2025-04-28 21:22:09,870 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s) and asserted 77 of 81 statements.
[2025-04-28 21:22:09,871 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 9 check-sat command(s)
[2025-04-28 21:22:09,871 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:09,873 INFO  L256         TraceCheckSpWp]: Trace formula consists of 277 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:09,875 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:09,950 INFO  L134       CoverageAnalysis]: Checked inductivity of 307 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 235 trivial. 0 not checked.
[2025-04-28 21:22:09,950 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
