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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:49,119 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:49,212 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1c3d9209-8d60-444a-a1da-9b624e198cf6/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:49,219 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:49,220 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:49,241 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:49,241 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:49,241 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:49,242 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:49,242 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:49,242 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:49,244 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:49,244 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:49,244 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:49,244 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:49,245 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:49,245 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:49,245 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:49,245 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:49,245 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:49,245 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:49,245 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:49,246 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:49,246 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:49,246 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:49,246 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:49,247 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:49,622 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:49,634 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:49,637 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:49,638 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:49,640 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:49,641 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1c3d9209-8d60-444a-a1da-9b624e198cf6/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-104.smt2
[2025-04-28 21:21:49,644 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:49,651 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:49,827 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1c3d9209-8d60-444a-a1da-9b624e198cf6/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-104.smt2
[2025-04-28 21:21:49,830 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:49,833 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:49,835 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:49,836 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:49,836 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:49,839 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,860 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49 Unit
[2025-04-28 21:21:49,861 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:49,863 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:49,863 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:49,863 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:49,881 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,881 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,911 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,911 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,912 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,913 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,916 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,917 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,918 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,934 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:49,935 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:49,936 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:49,936 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:49,938 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (1/1) ...
[2025-04-28 21:21:49,941 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:49,956 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:49,974 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:49,981 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:49,992 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:49,992 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:49,992 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:49,992 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:49,993 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:49,993 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:49,993 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:49,993 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:49,993 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:50,035 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:50,038 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:50,099 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:50,099 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:50,110 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:50,111 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:50,111 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:50 BoogieIcfgContainer
[2025-04-28 21:21:50,112 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:50,115 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:50,115 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:50,120 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:50,120 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:49" (1/3) ...
[2025-04-28 21:21:50,122 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@c3a9dab and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:50, skipping insertion in model container
[2025-04-28 21:21:50,122 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:49" (2/3) ...
[2025-04-28 21:21:50,123 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@c3a9dab and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:50, skipping insertion in model container
[2025-04-28 21:21:50,123 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:50" (3/3) ...
[2025-04-28 21:21:50,124 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:50,145 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:50,148 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 13 locations, 17 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:50,205 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:50,229 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;@73e88edb, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:50,230 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:50,235 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 13 states, 6 states have (on average 1.3333333333333333) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 2 states have return successors, (3), 3 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:50,246 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:50,246 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,248 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,248 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,256 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,257 INFO  L85        PathProgramCache]: Analyzing trace with hash -1672547219, now seen corresponding path program 1 times
[2025-04-28 21:21:50,268 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,268 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [639489767]
[2025-04-28 21:21:50,269 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,269 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,308 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:50,332 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:50,333 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,333 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,546 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:50,547 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,547 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [639489767]
[2025-04-28 21:21:50,548 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [639489767] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,548 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,551 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:50,553 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1096944804]
[2025-04-28 21:21:50,554 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,558 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:50,558 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,591 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:50,592 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:50,594 INFO  L87              Difference]: Start difference. First operand  has 13 states, 6 states have (on average 1.3333333333333333) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 2 states have return successors, (3), 3 states have call predecessors, (3), 3 states have call successors, (3) Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:50,645 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,645 INFO  L93              Difference]: Finished difference Result 13 states and 14 transitions.
[2025-04-28 21:21:50,648 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:50,651 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:50,652 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,660 INFO  L225             Difference]: With dead ends: 13
[2025-04-28 21:21:50,661 INFO  L226             Difference]: Without dead ends: 13
[2025-04-28 21:21:50,664 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:50,668 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 1 mSDsluCounter, 15 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 26 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,669 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 26 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:50,688 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 13 states.
[2025-04-28 21:21:50,710 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 13 to 13.
[2025-04-28 21:21:50,711 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 13 states, 6 states have (on average 1.1666666666666667) internal successors, (7), 7 states have internal predecessors, (7), 3 states have call successors, (3), 2 states have call predecessors, (3), 3 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:50,718 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 13 states to 13 states and 14 transitions.
[2025-04-28 21:21:50,719 INFO  L79                 Accepts]: Start accepts. Automaton has 13 states and 14 transitions. Word has length 9
[2025-04-28 21:21:50,719 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,720 INFO  L485      AbstractCegarLoop]: Abstraction has 13 states and 14 transitions.
[2025-04-28 21:21:50,720 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:50,720 INFO  L278                IsEmpty]: Start isEmpty. Operand 13 states and 14 transitions.
[2025-04-28 21:21:50,723 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:50,724 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,724 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,724 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:50,727 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,727 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,728 INFO  L85        PathProgramCache]: Analyzing trace with hash 13498287, now seen corresponding path program 1 times
[2025-04-28 21:21:50,728 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,728 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1131539622]
[2025-04-28 21:21:50,728 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,728 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,738 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:50,752 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:50,752 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,753 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,928 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:50,928 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,928 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1131539622]
[2025-04-28 21:21:50,928 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1131539622] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,929 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1838543197]
[2025-04-28 21:21:50,929 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,929 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,931 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,939 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:50,941 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,965 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:50,974 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:50,975 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,975 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,977 INFO  L256         TraceCheckSpWp]: Trace formula consists of 25 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,984 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:51,094 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:51,094 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,366 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:51,367 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1838543197] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,367 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,367 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:51,368 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [677022390]
[2025-04-28 21:21:51,368 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,368 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:51,369 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,369 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:51,369 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=16, Invalid=40, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:51,370 INFO  L87              Difference]: Start difference. First operand 13 states and 14 transitions. Second operand  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:51,424 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,424 INFO  L93              Difference]: Finished difference Result 15 states and 16 transitions.
[2025-04-28 21:21:51,425 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:51,425 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5) Word has length 13
[2025-04-28 21:21:51,425 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,426 INFO  L225             Difference]: With dead ends: 15
[2025-04-28 21:21:51,426 INFO  L226             Difference]: Without dead ends: 15
[2025-04-28 21:21:51,426 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 24 SyntacticMatches, 1 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:51,427 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 5 mSDsluCounter, 27 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 38 SdHoareTripleChecker+Invalid, 25 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 22 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,428 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 38 Invalid, 25 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:51,428 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15 states.
[2025-04-28 21:21:51,431 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15 to 15.
[2025-04-28 21:21:51,431 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 15 states, 7 states have (on average 1.1428571428571428) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:51,432 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 15 states to 15 states and 16 transitions.
[2025-04-28 21:21:51,432 INFO  L79                 Accepts]: Start accepts. Automaton has 15 states and 16 transitions. Word has length 13
[2025-04-28 21:21:51,432 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,432 INFO  L485      AbstractCegarLoop]: Abstraction has 15 states and 16 transitions.
[2025-04-28 21:21:51,433 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:51,433 INFO  L278                IsEmpty]: Start isEmpty. Operand 15 states and 16 transitions.
[2025-04-28 21:21:51,433 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:51,433 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,433 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,456 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:51,634 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:51,635 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,635 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,635 INFO  L85        PathProgramCache]: Analyzing trace with hash -1177266959, now seen corresponding path program 2 times
[2025-04-28 21:21:51,635 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,635 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1221621308]
[2025-04-28 21:21:51,636 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:51,636 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,643 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:51,649 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:51,652 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:51,652 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,881 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:51,881 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,882 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1221621308]
[2025-04-28 21:21:51,882 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1221621308] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:51,882 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1148058081]
[2025-04-28 21:21:51,882 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:51,882 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,886 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:51,888 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:51,892 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:51,919 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:51,928 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:51,929 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:51,929 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,931 INFO  L256         TraceCheckSpWp]: Trace formula consists of 33 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:51,933 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:51,989 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:51,989 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,316 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:52,316 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1148058081] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,316 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,316 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 11
[2025-04-28 21:21:52,318 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [394665895]
[2025-04-28 21:21:52,318 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,318 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:52,319 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,319 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:52,319 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=26, Invalid=84, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:52,320 INFO  L87              Difference]: Start difference. First operand 15 states and 16 transitions. Second operand  has 11 states, 5 states have (on average 2.4) internal successors, (12), 10 states have internal predecessors, (12), 7 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:52,413 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,414 INFO  L93              Difference]: Finished difference Result 17 states and 18 transitions.
[2025-04-28 21:21:52,415 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:52,415 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 5 states have (on average 2.4) internal successors, (12), 10 states have internal predecessors, (12), 7 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8) Word has length 17
[2025-04-28 21:21:52,416 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,416 INFO  L225             Difference]: With dead ends: 17
[2025-04-28 21:21:52,416 INFO  L226             Difference]: Without dead ends: 17
[2025-04-28 21:21:52,417 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 43 GetRequests, 32 SyntacticMatches, 0 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=38, Invalid=118, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:52,417 INFO  L437           NwaCegarLoop]: 12 mSDtfsCounter, 4 mSDsluCounter, 60 mSDsCounter, 0 mSdLazyCounter, 45 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 72 SdHoareTripleChecker+Invalid, 45 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 45 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,418 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 72 Invalid, 45 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 45 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:52,421 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17 states.
[2025-04-28 21:21:52,423 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 17 to 17.
[2025-04-28 21:21:52,423 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 17 states, 8 states have (on average 1.125) internal successors, (9), 9 states have internal predecessors, (9), 3 states have call successors, (3), 2 states have call predecessors, (3), 5 states have return successors, (6), 5 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:52,424 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 18 transitions.
[2025-04-28 21:21:52,427 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 18 transitions. Word has length 17
[2025-04-28 21:21:52,428 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,428 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 18 transitions.
[2025-04-28 21:21:52,428 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 5 states have (on average 2.4) internal successors, (12), 10 states have internal predecessors, (12), 7 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:52,428 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 18 transitions.
[2025-04-28 21:21:52,428 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:52,429 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,429 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,435 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:52,629 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:52,629 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,630 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,630 INFO  L85        PathProgramCache]: Analyzing trace with hash 329141299, now seen corresponding path program 3 times
[2025-04-28 21:21:52,630 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,630 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1017342691]
[2025-04-28 21:21:52,630 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:52,630 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,636 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:52,643 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:52,644 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:52,644 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,777 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 12 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:52,777 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,777 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1017342691]
[2025-04-28 21:21:52,778 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1017342691] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,778 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [483663771]
[2025-04-28 21:21:52,778 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:52,778 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,781 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,783 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:52,785 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,807 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:52,815 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:52,815 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:52,815 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,816 INFO  L256         TraceCheckSpWp]: Trace formula consists of 41 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,819 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,875 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 12 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:52,875 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,298 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 15 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:53,298 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [483663771] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,298 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,298 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 10] total 12
[2025-04-28 21:21:53,298 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1533391039]
[2025-04-28 21:21:53,299 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,299 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:53,299 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,303 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:53,303 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:53,303 INFO  L87              Difference]: Start difference. First operand 17 states and 18 transitions. Second operand  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:53,421 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,422 INFO  L93              Difference]: Finished difference Result 19 states and 20 transitions.
[2025-04-28 21:21:53,424 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:53,424 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9) Word has length 21
[2025-04-28 21:21:53,424 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,425 INFO  L225             Difference]: With dead ends: 19
[2025-04-28 21:21:53,425 INFO  L226             Difference]: Without dead ends: 19
[2025-04-28 21:21:53,425 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 40 SyntacticMatches, 1 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 9 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=49, Invalid=161, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:53,426 INFO  L437           NwaCegarLoop]: 13 mSDtfsCounter, 9 mSDsluCounter, 60 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 73 SdHoareTripleChecker+Invalid, 59 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,426 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 73 Invalid, 59 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:53,427 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 19 states.
[2025-04-28 21:21:53,432 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 19 to 19.
[2025-04-28 21:21:53,432 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 19 states, 9 states have (on average 1.1111111111111112) internal successors, (10), 10 states have internal predecessors, (10), 3 states have call successors, (3), 2 states have call predecessors, (3), 6 states have return successors, (7), 6 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:53,433 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 19 states to 19 states and 20 transitions.
[2025-04-28 21:21:53,433 INFO  L79                 Accepts]: Start accepts. Automaton has 19 states and 20 transitions. Word has length 21
[2025-04-28 21:21:53,433 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,433 INFO  L485      AbstractCegarLoop]: Abstraction has 19 states and 20 transitions.
[2025-04-28 21:21:53,435 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:53,436 INFO  L278                IsEmpty]: Start isEmpty. Operand 19 states and 20 transitions.
[2025-04-28 21:21:53,437 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:53,437 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,437 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,442 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:53,638 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:53,638 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,638 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,639 INFO  L85        PathProgramCache]: Analyzing trace with hash 1761090933, now seen corresponding path program 4 times
[2025-04-28 21:21:53,639 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,639 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [498009487]
[2025-04-28 21:21:53,639 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:53,639 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,644 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:53,660 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:53,661 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:53,661 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,012 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 23 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:54,012 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,012 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [498009487]
[2025-04-28 21:21:54,012 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [498009487] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,012 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [83491515]
[2025-04-28 21:21:54,013 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:54,013 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,016 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,018 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:54,023 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,052 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:54,061 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:54,061 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:54,061 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,062 INFO  L256         TraceCheckSpWp]: Trace formula consists of 49 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,063 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,129 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:54,130 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,662 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 26 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:54,662 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [83491515] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,662 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,662 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 12] total 15
[2025-04-28 21:21:54,663 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [582165103]
[2025-04-28 21:21:54,663 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,663 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:54,663 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,664 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:54,664 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=172, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:54,664 INFO  L87              Difference]: Start difference. First operand 19 states and 20 transitions. Second operand  has 15 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 14 states have internal predecessors, (16), 9 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (12), 5 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:54,811 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,813 INFO  L93              Difference]: Finished difference Result 21 states and 22 transitions.
[2025-04-28 21:21:54,814 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:54,814 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 14 states have internal predecessors, (16), 9 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (12), 5 states have call predecessors, (12), 9 states have call successors, (12) Word has length 25
[2025-04-28 21:21:54,815 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,815 INFO  L225             Difference]: With dead ends: 21
[2025-04-28 21:21:54,815 INFO  L226             Difference]: Without dead ends: 21
[2025-04-28 21:21:54,815 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 65 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=70, Invalid=272, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:54,816 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 14 mSDsluCounter, 90 mSDsCounter, 0 mSdLazyCounter, 77 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 104 SdHoareTripleChecker+Invalid, 87 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 77 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,816 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 104 Invalid, 87 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 77 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:54,817 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 21 states.
[2025-04-28 21:21:54,822 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 21 to 21.
[2025-04-28 21:21:54,824 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 21 states, 10 states have (on average 1.1) internal successors, (11), 11 states have internal predecessors, (11), 3 states have call successors, (3), 2 states have call predecessors, (3), 7 states have return successors, (8), 7 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:54,825 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 21 states to 21 states and 22 transitions.
[2025-04-28 21:21:54,825 INFO  L79                 Accepts]: Start accepts. Automaton has 21 states and 22 transitions. Word has length 25
[2025-04-28 21:21:54,825 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,826 INFO  L485      AbstractCegarLoop]: Abstraction has 21 states and 22 transitions.
[2025-04-28 21:21:54,826 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 14 states have internal predecessors, (16), 9 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (12), 5 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:54,826 INFO  L278                IsEmpty]: Start isEmpty. Operand 21 states and 22 transitions.
[2025-04-28 21:21:54,827 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:54,827 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,827 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,833 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:55,032 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:55,033 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,033 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,033 INFO  L85        PathProgramCache]: Analyzing trace with hash 1866336439, now seen corresponding path program 5 times
[2025-04-28 21:21:55,033 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,033 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [47605261]
[2025-04-28 21:21:55,033 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:55,033 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,038 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 29 statements into 6 equivalence classes.
[2025-04-28 21:21:55,043 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:55,044 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:55,044 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,308 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 30 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:55,308 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,308 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [47605261]
[2025-04-28 21:21:55,308 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [47605261] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,308 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [638289279]
[2025-04-28 21:21:55,308 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:55,309 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,311 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,314 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:55,318 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,348 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 29 statements into 6 equivalence classes.
[2025-04-28 21:21:55,360 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:55,360 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:55,360 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,361 INFO  L256         TraceCheckSpWp]: Trace formula consists of 57 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,364 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,456 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 30 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:55,457 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,179 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 40 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:56,179 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [638289279] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,179 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,179 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 14] total 17
[2025-04-28 21:21:56,179 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1767933179]
[2025-04-28 21:21:56,179 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,180 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:56,180 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,181 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:56,181 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=44, Invalid=228, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:56,181 INFO  L87              Difference]: Start difference. First operand 21 states and 22 transitions. Second operand  has 17 states, 8 states have (on average 2.25) internal successors, (18), 16 states have internal predecessors, (18), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (14), 6 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:21:56,351 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,351 INFO  L93              Difference]: Finished difference Result 23 states and 24 transitions.
[2025-04-28 21:21:56,351 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:56,352 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.25) internal successors, (18), 16 states have internal predecessors, (18), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (14), 6 states have call predecessors, (14), 10 states have call successors, (14) Word has length 29
[2025-04-28 21:21:56,352 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,352 INFO  L225             Difference]: With dead ends: 23
[2025-04-28 21:21:56,352 INFO  L226             Difference]: Without dead ends: 23
[2025-04-28 21:21:56,353 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 76 GetRequests, 56 SyntacticMatches, 0 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 37 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=89, Invalid=373, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:56,354 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 29 mSDsluCounter, 90 mSDsCounter, 0 mSdLazyCounter, 86 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 37 SdHoareTripleChecker+Valid, 105 SdHoareTripleChecker+Invalid, 112 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 86 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,354 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [37 Valid, 105 Invalid, 112 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 86 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:56,355 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 23 states.
[2025-04-28 21:21:56,358 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 23 to 23.
[2025-04-28 21:21:56,358 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 23 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 3 states have call successors, (3), 2 states have call predecessors, (3), 8 states have return successors, (9), 8 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:56,359 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 23 states to 23 states and 24 transitions.
[2025-04-28 21:21:56,359 INFO  L79                 Accepts]: Start accepts. Automaton has 23 states and 24 transitions. Word has length 29
[2025-04-28 21:21:56,359 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,359 INFO  L485      AbstractCegarLoop]: Abstraction has 23 states and 24 transitions.
[2025-04-28 21:21:56,359 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.25) internal successors, (18), 16 states have internal predecessors, (18), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (14), 6 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:21:56,359 INFO  L278                IsEmpty]: Start isEmpty. Operand 23 states and 24 transitions.
[2025-04-28 21:21:56,360 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:56,360 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,360 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,366 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:56,564 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:56,565 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,565 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,566 INFO  L85        PathProgramCache]: Analyzing trace with hash -2107879943, now seen corresponding path program 6 times
[2025-04-28 21:21:56,566 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,566 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [575300523]
[2025-04-28 21:21:56,566 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:56,566 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,571 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:56,580 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:56,580 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:56,580 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,840 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 42 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:56,840 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,840 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [575300523]
[2025-04-28 21:21:56,840 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [575300523] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,841 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1391341495]
[2025-04-28 21:21:56,841 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:56,841 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,843 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,845 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:56,849 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,887 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:56,904 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:56,904 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:56,904 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,905 INFO  L256         TraceCheckSpWp]: Trace formula consists of 65 conjuncts, 29 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,907 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,973 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 42 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:56,973 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:57,868 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 57 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:21:57,869 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1391341495] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:57,869 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:57,869 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 16] total 18
[2025-04-28 21:21:57,869 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1785377761]
[2025-04-28 21:21:57,869 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,870 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:57,870 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,871 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:57,871 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=260, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:57,871 INFO  L87              Difference]: Start difference. First operand 23 states and 24 transitions. Second operand  has 18 states, 9 states have (on average 2.111111111111111) internal successors, (19), 17 states have internal predecessors, (19), 10 states have call successors, (10), 1 states have call predecessors, (10), 8 states have return successors, (15), 7 states have call predecessors, (15), 10 states have call successors, (15)
[2025-04-28 21:21:58,074 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,075 INFO  L93              Difference]: Finished difference Result 25 states and 26 transitions.
[2025-04-28 21:21:58,075 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:58,076 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 9 states have (on average 2.111111111111111) internal successors, (19), 17 states have internal predecessors, (19), 10 states have call successors, (10), 1 states have call predecessors, (10), 8 states have return successors, (15), 7 states have call predecessors, (15), 10 states have call successors, (15) Word has length 33
[2025-04-28 21:21:58,077 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,078 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:21:58,081 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:21:58,081 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 87 GetRequests, 64 SyntacticMatches, 1 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=106, Invalid=446, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:58,082 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 26 mSDsluCounter, 127 mSDsCounter, 0 mSdLazyCounter, 117 mSolverCounterSat, 21 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 35 SdHoareTripleChecker+Valid, 143 SdHoareTripleChecker+Invalid, 138 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 21 IncrementalHoareTripleChecker+Valid, 117 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,082 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [35 Valid, 143 Invalid, 138 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [21 Valid, 117 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:58,083 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:21:58,089 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 25.
[2025-04-28 21:21:58,089 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 25 states, 12 states have (on average 1.0833333333333333) internal successors, (13), 13 states have internal predecessors, (13), 3 states have call successors, (3), 2 states have call predecessors, (3), 9 states have return successors, (10), 9 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:58,090 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 26 transitions.
[2025-04-28 21:21:58,093 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 26 transitions. Word has length 33
[2025-04-28 21:21:58,093 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,093 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 26 transitions.
[2025-04-28 21:21:58,093 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 9 states have (on average 2.111111111111111) internal successors, (19), 17 states have internal predecessors, (19), 10 states have call successors, (10), 1 states have call predecessors, (10), 8 states have return successors, (15), 7 states have call predecessors, (15), 10 states have call successors, (15)
[2025-04-28 21:21:58,094 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 26 transitions.
[2025-04-28 21:21:58,094 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:21:58,094 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,095 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,100 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:58,295 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:58,295 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,296 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,296 INFO  L85        PathProgramCache]: Analyzing trace with hash -254857925, now seen corresponding path program 7 times
[2025-04-28 21:21:58,296 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,296 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [408372102]
[2025-04-28 21:21:58,296 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:58,296 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,300 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:58,307 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:58,307 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,307 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,548 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 56 refuted. 0 times theorem prover too weak. 49 trivial. 0 not checked.
[2025-04-28 21:21:58,548 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,548 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [408372102]
[2025-04-28 21:21:58,548 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [408372102] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,548 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1899760422]
[2025-04-28 21:21:58,548 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:58,548 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,551 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:58,553 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:58,558 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,598 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 37 statements into 1 equivalence classes.
[2025-04-28 21:21:58,609 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:21:58,609 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,610 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,611 INFO  L256         TraceCheckSpWp]: Trace formula consists of 73 conjuncts, 33 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,615 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,688 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 56 refuted. 0 times theorem prover too weak. 49 trivial. 0 not checked.
[2025-04-28 21:21:58,688 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,763 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 77 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:21:59,763 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1899760422] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,763 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,763 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 18] total 20
[2025-04-28 21:21:59,764 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [140575253]
[2025-04-28 21:21:59,764 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,764 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:59,764 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,767 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:59,767 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=52, Invalid=328, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:59,767 INFO  L87              Difference]: Start difference. First operand 25 states and 26 transitions. Second operand  has 20 states, 10 states have (on average 2.1) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:59,968 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,968 INFO  L93              Difference]: Finished difference Result 27 states and 28 transitions.
[2025-04-28 21:21:59,969 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:59,969 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.1) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17) Word has length 37
[2025-04-28 21:21:59,970 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,970 INFO  L225             Difference]: With dead ends: 27
[2025-04-28 21:21:59,972 INFO  L226             Difference]: Without dead ends: 27
[2025-04-28 21:21:59,972 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 98 GetRequests, 72 SyntacticMatches, 1 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 49 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=129, Invalid=573, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:59,973 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 45 mSDsluCounter, 134 mSDsCounter, 0 mSdLazyCounter, 130 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 55 SdHoareTripleChecker+Valid, 151 SdHoareTripleChecker+Invalid, 171 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 130 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,974 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [55 Valid, 151 Invalid, 171 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 130 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:59,975 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 27 states.
[2025-04-28 21:21:59,978 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 27 to 27.
[2025-04-28 21:21:59,980 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 27 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 3 states have call successors, (3), 2 states have call predecessors, (3), 10 states have return successors, (11), 10 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:59,981 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 27 states to 27 states and 28 transitions.
[2025-04-28 21:21:59,981 INFO  L79                 Accepts]: Start accepts. Automaton has 27 states and 28 transitions. Word has length 37
[2025-04-28 21:21:59,981 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,982 INFO  L485      AbstractCegarLoop]: Abstraction has 27 states and 28 transitions.
[2025-04-28 21:21:59,982 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.1) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (11), 1 states have call predecessors, (11), 9 states have return successors, (17), 8 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:59,983 INFO  L278                IsEmpty]: Start isEmpty. Operand 27 states and 28 transitions.
[2025-04-28 21:21:59,983 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 42
[2025-04-28 21:21:59,984 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,984 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,989 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:00,186 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:22:00,187 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:00,187 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:00,187 INFO  L85        PathProgramCache]: Analyzing trace with hash 1201858173, now seen corresponding path program 8 times
[2025-04-28 21:22:00,187 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:00,187 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [283716111]
[2025-04-28 21:22:00,187 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:00,188 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:00,191 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 41 statements into 2 equivalence classes.
[2025-04-28 21:22:00,198 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:22:00,198 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:00,198 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,435 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 64 trivial. 0 not checked.
[2025-04-28 21:22:00,435 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,435 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [283716111]
[2025-04-28 21:22:00,435 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [283716111] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,435 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2135415499]
[2025-04-28 21:22:00,435 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:00,436 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,438 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,441 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:22:00,445 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,492 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 41 statements into 2 equivalence classes.
[2025-04-28 21:22:00,508 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 41 of 41 statements.
[2025-04-28 21:22:00,508 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:00,508 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,509 INFO  L256         TraceCheckSpWp]: Trace formula consists of 81 conjuncts, 37 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,512 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,586 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 72 refuted. 0 times theorem prover too weak. 64 trivial. 0 not checked.
[2025-04-28 21:22:00,586 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,762 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 0 proven. 100 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:22:01,762 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2135415499] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,762 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,762 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 20] total 22
[2025-04-28 21:22:01,762 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1943567816]
[2025-04-28 21:22:01,763 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,763 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:22:01,763 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,764 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:22:01,764 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=404, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:22:01,764 INFO  L87              Difference]: Start difference. First operand 27 states and 28 transitions. Second operand  has 22 states, 11 states have (on average 2.090909090909091) internal successors, (23), 21 states have internal predecessors, (23), 12 states have call successors, (12), 1 states have call predecessors, (12), 10 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19)
[2025-04-28 21:22:01,994 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,994 INFO  L93              Difference]: Finished difference Result 29 states and 30 transitions.
[2025-04-28 21:22:01,995 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:01,995 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 2.090909090909091) internal successors, (23), 21 states have internal predecessors, (23), 12 states have call successors, (12), 1 states have call predecessors, (12), 10 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19) Word has length 41
[2025-04-28 21:22:01,996 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,997 INFO  L225             Difference]: With dead ends: 29
[2025-04-28 21:22:01,997 INFO  L226             Difference]: Without dead ends: 29
[2025-04-28 21:22:01,997 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 109 GetRequests, 80 SyntacticMatches, 1 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 64 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=154, Invalid=716, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:22:01,998 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 75 mSDsluCounter, 168 mSDsCounter, 0 mSdLazyCounter, 161 mSolverCounterSat, 73 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 86 SdHoareTripleChecker+Valid, 186 SdHoareTripleChecker+Invalid, 234 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 73 IncrementalHoareTripleChecker+Valid, 161 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,998 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [86 Valid, 186 Invalid, 234 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [73 Valid, 161 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:01,999 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 29 states.
[2025-04-28 21:22:02,002 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 29 to 29.
[2025-04-28 21:22:02,002 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 29 states, 14 states have (on average 1.0714285714285714) internal successors, (15), 15 states have internal predecessors, (15), 3 states have call successors, (3), 2 states have call predecessors, (3), 11 states have return successors, (12), 11 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:22:02,003 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 29 states to 29 states and 30 transitions.
[2025-04-28 21:22:02,003 INFO  L79                 Accepts]: Start accepts. Automaton has 29 states and 30 transitions. Word has length 41
[2025-04-28 21:22:02,003 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:02,003 INFO  L485      AbstractCegarLoop]: Abstraction has 29 states and 30 transitions.
[2025-04-28 21:22:02,003 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 2.090909090909091) internal successors, (23), 21 states have internal predecessors, (23), 12 states have call successors, (12), 1 states have call predecessors, (12), 10 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19)
[2025-04-28 21:22:02,003 INFO  L278                IsEmpty]: Start isEmpty. Operand 29 states and 30 transitions.
[2025-04-28 21:22:02,004 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 46
[2025-04-28 21:22:02,004 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:02,004 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:02,009 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:22:02,208 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,209 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,209 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,209 INFO  L85        PathProgramCache]: Analyzing trace with hash -1636582977, now seen corresponding path program 9 times
[2025-04-28 21:22:02,209 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,209 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1917820088]
[2025-04-28 21:22:02,209 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:02,209 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,213 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 45 statements into 10 equivalence classes.
[2025-04-28 21:22:02,222 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:22:02,222 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:22:02,222 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,476 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:22:02,476 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,477 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1917820088]
[2025-04-28 21:22:02,477 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1917820088] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,477 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1267941301]
[2025-04-28 21:22:02,477 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:02,477 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,480 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:02,482 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,485 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,530 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 45 statements into 10 equivalence classes.
[2025-04-28 21:22:02,549 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 45 of 45 statements.
[2025-04-28 21:22:02,549 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:22:02,549 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,550 INFO  L256         TraceCheckSpWp]: Trace formula consists of 89 conjuncts, 41 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,552 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,628 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:22:02,628 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:04,025 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 126 refuted. 0 times theorem prover too weak. 45 trivial. 0 not checked.
[2025-04-28 21:22:04,026 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1267941301] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:04,026 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:04,026 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 22] total 24
[2025-04-28 21:22:04,026 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [936606466]
[2025-04-28 21:22:04,026 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:04,026 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 24 states
[2025-04-28 21:22:04,026 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:04,027 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2025-04-28 21:22:04,027 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=64, Invalid=488, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:22:04,028 INFO  L87              Difference]: Start difference. First operand 29 states and 30 transitions. Second operand  has 24 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 13 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:22:04,287 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,287 INFO  L93              Difference]: Finished difference Result 31 states and 32 transitions.
[2025-04-28 21:22:04,287 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:22:04,288 INFO  L79                 Accepts]: Start accepts. Automaton has  has 24 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 13 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21) Word has length 45
[2025-04-28 21:22:04,288 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,288 INFO  L225             Difference]: With dead ends: 31
[2025-04-28 21:22:04,289 INFO  L226             Difference]: Without dead ends: 31
[2025-04-28 21:22:04,290 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 120 GetRequests, 88 SyntacticMatches, 1 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 81 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=181, Invalid=875, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:22:04,290 INFO  L437           NwaCegarLoop]: 19 mSDtfsCounter, 48 mSDsluCounter, 186 mSDsCounter, 0 mSdLazyCounter, 182 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 60 SdHoareTripleChecker+Valid, 205 SdHoareTripleChecker+Invalid, 223 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 182 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,291 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [60 Valid, 205 Invalid, 223 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 182 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:04,291 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 31 states.
[2025-04-28 21:22:04,298 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 31 to 31.
[2025-04-28 21:22:04,299 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 31 states, 15 states have (on average 1.0666666666666667) internal successors, (16), 16 states have internal predecessors, (16), 3 states have call successors, (3), 2 states have call predecessors, (3), 12 states have return successors, (13), 12 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:22:04,299 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 31 states to 31 states and 32 transitions.
[2025-04-28 21:22:04,302 INFO  L79                 Accepts]: Start accepts. Automaton has 31 states and 32 transitions. Word has length 45
[2025-04-28 21:22:04,302 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,302 INFO  L485      AbstractCegarLoop]: Abstraction has 31 states and 32 transitions.
[2025-04-28 21:22:04,303 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 24 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 13 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (21), 10 states have call predecessors, (21), 13 states have call successors, (21)
[2025-04-28 21:22:04,303 INFO  L278                IsEmpty]: Start isEmpty. Operand 31 states and 32 transitions.
[2025-04-28 21:22:04,304 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 50
[2025-04-28 21:22:04,304 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,304 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:04,309 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:22:04,504 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:04,504 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,505 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,505 INFO  L85        PathProgramCache]: Analyzing trace with hash -479336703, now seen corresponding path program 10 times
[2025-04-28 21:22:04,505 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,505 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [823695846]
[2025-04-28 21:22:04,505 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:04,505 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,508 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 49 statements into 2 equivalence classes.
[2025-04-28 21:22:04,512 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:22:04,512 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:04,512 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,905 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 119 refuted. 0 times theorem prover too weak. 91 trivial. 0 not checked.
[2025-04-28 21:22:04,905 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,905 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [823695846]
[2025-04-28 21:22:04,905 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [823695846] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:04,905 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [730935094]
[2025-04-28 21:22:04,906 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:04,906 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,908 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:04,910 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:04,914 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:04,964 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 49 statements into 2 equivalence classes.
[2025-04-28 21:22:04,977 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 49 of 49 statements.
[2025-04-28 21:22:04,977 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:04,977 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,978 INFO  L256         TraceCheckSpWp]: Trace formula consists of 97 conjuncts, 45 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:04,980 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:05,062 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 100 trivial. 0 not checked.
[2025-04-28 21:22:05,062 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:06,686 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 0 proven. 155 refuted. 0 times theorem prover too weak. 55 trivial. 0 not checked.
[2025-04-28 21:22:06,686 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [730935094] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:06,686 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:06,687 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 15, 24] total 27
[2025-04-28 21:22:06,687 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [149667053]
[2025-04-28 21:22:06,687 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:06,687 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:22:06,687 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:06,688 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:22:06,688 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=74, Invalid=628, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:06,689 INFO  L87              Difference]: Start difference. First operand 31 states and 32 transitions. Second operand  has 27 states, 13 states have (on average 2.1538461538461537) internal successors, (28), 26 states have internal predecessors, (28), 15 states have call successors, (15), 1 states have call predecessors, (15), 12 states have return successors, (24), 11 states have call predecessors, (24), 15 states have call successors, (24)
[2025-04-28 21:22:06,966 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,966 INFO  L93              Difference]: Finished difference Result 33 states and 34 transitions.
[2025-04-28 21:22:06,967 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 15 states. 
[2025-04-28 21:22:06,968 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 13 states have (on average 2.1538461538461537) internal successors, (28), 26 states have internal predecessors, (28), 15 states have call successors, (15), 1 states have call predecessors, (15), 12 states have return successors, (24), 11 states have call predecessors, (24), 15 states have call successors, (24) Word has length 49
[2025-04-28 21:22:06,968 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,969 INFO  L225             Difference]: With dead ends: 33
[2025-04-28 21:22:06,969 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:22:06,969 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 131 GetRequests, 96 SyntacticMatches, 0 SemanticMatches, 35 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 144 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=214, Invalid=1118, Unknown=0, NotChecked=0, Total=1332
[2025-04-28 21:22:06,970 INFO  L437           NwaCegarLoop]: 20 mSDtfsCounter, 32 mSDsluCounter, 247 mSDsCounter, 0 mSdLazyCounter, 233 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 45 SdHoareTripleChecker+Valid, 267 SdHoareTripleChecker+Invalid, 255 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 233 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,970 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [45 Valid, 267 Invalid, 255 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 233 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:06,970 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:22:06,976 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 33.
[2025-04-28 21:22:06,977 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 16 states have (on average 1.0625) internal successors, (17), 17 states have internal predecessors, (17), 3 states have call successors, (3), 2 states have call predecessors, (3), 13 states have return successors, (14), 13 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:22:06,981 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 34 transitions.
[2025-04-28 21:22:06,982 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 34 transitions. Word has length 49
[2025-04-28 21:22:06,982 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,982 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 34 transitions.
[2025-04-28 21:22:06,982 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 13 states have (on average 2.1538461538461537) internal successors, (28), 26 states have internal predecessors, (28), 15 states have call successors, (15), 1 states have call predecessors, (15), 12 states have return successors, (24), 11 states have call predecessors, (24), 15 states have call successors, (24)
[2025-04-28 21:22:06,982 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 34 transitions.
[2025-04-28 21:22:06,983 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 54
[2025-04-28 21:22:06,983 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,983 INFO  L218           NwaCegarLoop]: trace histogram [12, 11, 11, 11, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:06,991 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-04-28 21:22:07,183 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,184 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:07,184 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:07,184 INFO  L85        PathProgramCache]: Analyzing trace with hash 659402307, now seen corresponding path program 11 times
[2025-04-28 21:22:07,184 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:07,184 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1000159655]
[2025-04-28 21:22:07,184 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:22:07,184 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:07,188 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 53 statements into 12 equivalence classes.
[2025-04-28 21:22:07,202 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 12 check-sat command(s) and asserted 53 of 53 statements.
[2025-04-28 21:22:07,202 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 12 check-sat command(s)
[2025-04-28 21:22:07,202 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,501 INFO  L134       CoverageAnalysis]: Checked inductivity of 253 backedges. 0 proven. 132 refuted. 0 times theorem prover too weak. 121 trivial. 0 not checked.
[2025-04-28 21:22:07,501 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,501 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1000159655]
[2025-04-28 21:22:07,502 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1000159655] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,502 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1034612375]
[2025-04-28 21:22:07,502 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:22:07,502 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,504 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:07,506 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:07,509 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,565 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 53 statements into 12 equivalence classes.
[2025-04-28 21:22:07,584 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 12 check-sat command(s) and asserted 53 of 53 statements.
[2025-04-28 21:22:07,584 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 12 check-sat command(s)
[2025-04-28 21:22:07,584 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,585 INFO  L256         TraceCheckSpWp]: Trace formula consists of 105 conjuncts, 49 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,587 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:07,682 INFO  L134       CoverageAnalysis]: Checked inductivity of 253 backedges. 0 proven. 132 refuted. 0 times theorem prover too weak. 121 trivial. 0 not checked.
[2025-04-28 21:22:07,682 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:09,414 INFO  L134       CoverageAnalysis]: Checked inductivity of 253 backedges. 0 proven. 187 refuted. 0 times theorem prover too weak. 66 trivial. 0 not checked.
[2025-04-28 21:22:09,414 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1034612375] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:09,414 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:09,414 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 16, 26] total 29
[2025-04-28 21:22:09,414 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [159106413]
[2025-04-28 21:22:09,414 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:09,415 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 29 states
[2025-04-28 21:22:09,415 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:09,416 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 29 interpolants.
[2025-04-28 21:22:09,416 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=80, Invalid=732, Unknown=0, NotChecked=0, Total=812
[2025-04-28 21:22:09,416 INFO  L87              Difference]: Start difference. First operand 33 states and 34 transitions. Second operand  has 29 states, 14 states have (on average 2.142857142857143) internal successors, (30), 28 states have internal predecessors, (30), 16 states have call successors, (16), 1 states have call predecessors, (16), 13 states have return successors, (26), 12 states have call predecessors, (26), 16 states have call successors, (26)
[2025-04-28 21:22:09,695 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:09,696 INFO  L93              Difference]: Finished difference Result 35 states and 36 transitions.
[2025-04-28 21:22:09,696 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:22:09,696 INFO  L79                 Accepts]: Start accepts. Automaton has  has 29 states, 14 states have (on average 2.142857142857143) internal successors, (30), 28 states have internal predecessors, (30), 16 states have call successors, (16), 1 states have call predecessors, (16), 13 states have return successors, (26), 12 states have call predecessors, (26), 16 states have call successors, (26) Word has length 53
[2025-04-28 21:22:09,697 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:09,697 INFO  L225             Difference]: With dead ends: 35
[2025-04-28 21:22:09,697 INFO  L226             Difference]: Without dead ends: 35
[2025-04-28 21:22:09,698 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 142 GetRequests, 104 SyntacticMatches, 0 SemanticMatches, 38 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 145 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=245, Invalid=1315, Unknown=0, NotChecked=0, Total=1560
[2025-04-28 21:22:09,698 INFO  L437           NwaCegarLoop]: 21 mSDtfsCounter, 36 mSDsluCounter, 264 mSDsCounter, 0 mSdLazyCounter, 255 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 50 SdHoareTripleChecker+Valid, 285 SdHoareTripleChecker+Invalid, 280 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 255 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:09,698 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [50 Valid, 285 Invalid, 280 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 255 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:09,699 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 35 states.
[2025-04-28 21:22:09,702 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 35 to 35.
[2025-04-28 21:22:09,702 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 35 states, 17 states have (on average 1.0588235294117647) internal successors, (18), 18 states have internal predecessors, (18), 3 states have call successors, (3), 2 states have call predecessors, (3), 14 states have return successors, (15), 14 states have call predecessors, (15), 3 states have call successors, (15)
[2025-04-28 21:22:09,703 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 35 states to 35 states and 36 transitions.
[2025-04-28 21:22:09,703 INFO  L79                 Accepts]: Start accepts. Automaton has 35 states and 36 transitions. Word has length 53
[2025-04-28 21:22:09,703 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:09,703 INFO  L485      AbstractCegarLoop]: Abstraction has 35 states and 36 transitions.
[2025-04-28 21:22:09,704 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 29 states, 14 states have (on average 2.142857142857143) internal successors, (30), 28 states have internal predecessors, (30), 16 states have call successors, (16), 1 states have call predecessors, (16), 13 states have return successors, (26), 12 states have call predecessors, (26), 16 states have call successors, (26)
[2025-04-28 21:22:09,704 INFO  L278                IsEmpty]: Start isEmpty. Operand 35 states and 36 transitions.
[2025-04-28 21:22:09,705 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 58
[2025-04-28 21:22:09,705 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:09,705 INFO  L218           NwaCegarLoop]: trace histogram [13, 12, 12, 12, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:09,709 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:09,906 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:22:09,907 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:09,907 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:09,907 INFO  L85        PathProgramCache]: Analyzing trace with hash -379629691, now seen corresponding path program 12 times
[2025-04-28 21:22:09,907 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:09,907 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [63928587]
[2025-04-28 21:22:09,907 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:22:09,907 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:09,910 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 57 statements into 13 equivalence classes.
[2025-04-28 21:22:09,921 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 13 check-sat command(s) and asserted 57 of 57 statements.
[2025-04-28 21:22:09,924 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 13 check-sat command(s)
[2025-04-28 21:22:09,924 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,273 INFO  L134       CoverageAnalysis]: Checked inductivity of 300 backedges. 0 proven. 156 refuted. 0 times theorem prover too weak. 144 trivial. 0 not checked.
[2025-04-28 21:22:10,273 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:10,273 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [63928587]
[2025-04-28 21:22:10,274 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [63928587] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:10,274 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1798986597]
[2025-04-28 21:22:10,274 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:22:10,274 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:10,277 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:10,279 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:10,283 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-04-28 21:22:10,354 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 57 statements into 13 equivalence classes.
[2025-04-28 21:22:10,372 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 13 check-sat command(s) and asserted 57 of 57 statements.
[2025-04-28 21:22:10,373 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 13 check-sat command(s)
[2025-04-28 21:22:10,373 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:10,374 INFO  L256         TraceCheckSpWp]: Trace formula consists of 113 conjuncts, 53 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:10,376 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:10,449 INFO  L134       CoverageAnalysis]: Checked inductivity of 300 backedges. 0 proven. 156 refuted. 0 times theorem prover too weak. 144 trivial. 0 not checked.
[2025-04-28 21:22:10,449 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:12,356 INFO  L134       CoverageAnalysis]: Checked inductivity of 300 backedges. 0 proven. 222 refuted. 0 times theorem prover too weak. 78 trivial. 0 not checked.
[2025-04-28 21:22:12,357 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1798986597] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:12,357 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:12,357 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [17, 17, 28] total 30
[2025-04-28 21:22:12,358 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1271095898]
[2025-04-28 21:22:12,358 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:12,358 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-04-28 21:22:12,358 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:12,359 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-04-28 21:22:12,359 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=82, Invalid=788, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:22:12,359 INFO  L87              Difference]: Start difference. First operand 35 states and 36 transitions. Second operand  has 30 states, 15 states have (on average 2.066666666666667) internal successors, (31), 29 states have internal predecessors, (31), 16 states have call successors, (16), 1 states have call predecessors, (16), 14 states have return successors, (27), 13 states have call predecessors, (27), 16 states have call successors, (27)
[2025-04-28 21:22:12,827 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:12,827 INFO  L93              Difference]: Finished difference Result 37 states and 38 transitions.
[2025-04-28 21:22:12,828 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 17 states. 
[2025-04-28 21:22:12,828 INFO  L79                 Accepts]: Start accepts. Automaton has  has 30 states, 15 states have (on average 2.066666666666667) internal successors, (31), 29 states have internal predecessors, (31), 16 states have call successors, (16), 1 states have call predecessors, (16), 14 states have return successors, (27), 13 states have call predecessors, (27), 16 states have call successors, (27) Word has length 57
[2025-04-28 21:22:12,828 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:12,829 INFO  L225             Difference]: With dead ends: 37
[2025-04-28 21:22:12,829 INFO  L226             Difference]: Without dead ends: 37
[2025-04-28 21:22:12,829 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 153 GetRequests, 112 SyntacticMatches, 1 SemanticMatches, 40 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 144 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=274, Invalid=1448, Unknown=0, NotChecked=0, Total=1722
[2025-04-28 21:22:12,830 INFO  L437           NwaCegarLoop]: 22 mSDtfsCounter, 158 mSDsluCounter, 289 mSDsCounter, 0 mSdLazyCounter, 283 mSolverCounterSat, 156 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 173 SdHoareTripleChecker+Valid, 311 SdHoareTripleChecker+Invalid, 439 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 156 IncrementalHoareTripleChecker+Valid, 283 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:12,832 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [173 Valid, 311 Invalid, 439 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [156 Valid, 283 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:12,832 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 37 states.
[2025-04-28 21:22:12,835 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 37 to 37.
[2025-04-28 21:22:12,838 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 37 states, 18 states have (on average 1.0555555555555556) internal successors, (19), 19 states have internal predecessors, (19), 3 states have call successors, (3), 2 states have call predecessors, (3), 15 states have return successors, (16), 15 states have call predecessors, (16), 3 states have call successors, (16)
[2025-04-28 21:22:12,838 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 37 states to 37 states and 38 transitions.
[2025-04-28 21:22:12,839 INFO  L79                 Accepts]: Start accepts. Automaton has 37 states and 38 transitions. Word has length 57
[2025-04-28 21:22:12,840 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:12,840 INFO  L485      AbstractCegarLoop]: Abstraction has 37 states and 38 transitions.
[2025-04-28 21:22:12,840 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 30 states, 15 states have (on average 2.066666666666667) internal successors, (31), 29 states have internal predecessors, (31), 16 states have call successors, (16), 1 states have call predecessors, (16), 14 states have return successors, (27), 13 states have call predecessors, (27), 16 states have call successors, (27)
[2025-04-28 21:22:12,840 INFO  L278                IsEmpty]: Start isEmpty. Operand 37 states and 38 transitions.
[2025-04-28 21:22:12,841 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 62
[2025-04-28 21:22:12,844 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:12,844 INFO  L218           NwaCegarLoop]: trace histogram [14, 13, 13, 13, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:12,850 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Ended with exit code 0
[2025-04-28 21:22:13,045 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,13 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,045 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:13,045 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:13,045 INFO  L85        PathProgramCache]: Analyzing trace with hash 1669270215, now seen corresponding path program 13 times
[2025-04-28 21:22:13,045 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:13,045 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2000894789]
[2025-04-28 21:22:13,046 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:13,046 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:13,049 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 61 statements into 1 equivalence classes.
[2025-04-28 21:22:13,055 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 61 of 61 statements.
[2025-04-28 21:22:13,055 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,055 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,395 INFO  L134       CoverageAnalysis]: Checked inductivity of 351 backedges. 0 proven. 182 refuted. 0 times theorem prover too weak. 169 trivial. 0 not checked.
[2025-04-28 21:22:13,395 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:13,395 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2000894789]
[2025-04-28 21:22:13,395 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2000894789] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:13,395 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [974637894]
[2025-04-28 21:22:13,395 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:13,396 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:13,398 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:13,400 INFO  L229       MonitoredProcess]: Starting monitored process 14 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:13,403 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Waiting until timeout for monitored process
[2025-04-28 21:22:13,479 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 61 statements into 1 equivalence classes.
[2025-04-28 21:22:13,495 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 61 of 61 statements.
[2025-04-28 21:22:13,495 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:13,495 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:13,496 INFO  L256         TraceCheckSpWp]: Trace formula consists of 121 conjuncts, 57 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:13,498 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:13,584 INFO  L134       CoverageAnalysis]: Checked inductivity of 351 backedges. 0 proven. 182 refuted. 0 times theorem prover too weak. 169 trivial. 0 not checked.
[2025-04-28 21:22:13,584 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:15,764 INFO  L134       CoverageAnalysis]: Checked inductivity of 351 backedges. 0 proven. 260 refuted. 0 times theorem prover too weak. 91 trivial. 0 not checked.
[2025-04-28 21:22:15,764 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [974637894] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:15,765 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:15,765 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [18, 18, 30] total 32
[2025-04-28 21:22:15,765 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [78791069]
[2025-04-28 21:22:15,765 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:15,765 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 32 states
[2025-04-28 21:22:15,765 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:15,766 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 32 interpolants.
[2025-04-28 21:22:15,766 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=88, Invalid=904, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:22:15,766 INFO  L87              Difference]: Start difference. First operand 37 states and 38 transitions. Second operand  has 32 states, 16 states have (on average 2.0625) internal successors, (33), 31 states have internal predecessors, (33), 17 states have call successors, (17), 1 states have call predecessors, (17), 15 states have return successors, (29), 14 states have call predecessors, (29), 17 states have call successors, (29)
[2025-04-28 21:22:16,263 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:16,263 INFO  L93              Difference]: Finished difference Result 39 states and 40 transitions.
[2025-04-28 21:22:16,263 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:22:16,264 INFO  L79                 Accepts]: Start accepts. Automaton has  has 32 states, 16 states have (on average 2.0625) internal successors, (33), 31 states have internal predecessors, (33), 17 states have call successors, (17), 1 states have call predecessors, (17), 15 states have return successors, (29), 14 states have call predecessors, (29), 17 states have call successors, (29) Word has length 61
[2025-04-28 21:22:16,264 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:16,264 INFO  L225             Difference]: With dead ends: 39
[2025-04-28 21:22:16,265 INFO  L226             Difference]: Without dead ends: 39
[2025-04-28 21:22:16,265 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 164 GetRequests, 120 SyntacticMatches, 1 SemanticMatches, 43 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 169 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=309, Invalid=1671, Unknown=0, NotChecked=0, Total=1980
[2025-04-28 21:22:16,266 INFO  L437           NwaCegarLoop]: 23 mSDtfsCounter, 81 mSDsluCounter, 314 mSDsCounter, 0 mSdLazyCounter, 310 mSolverCounterSat, 71 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 97 SdHoareTripleChecker+Valid, 337 SdHoareTripleChecker+Invalid, 381 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 71 IncrementalHoareTripleChecker+Valid, 310 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:16,266 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [97 Valid, 337 Invalid, 381 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [71 Valid, 310 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:16,267 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 39 states.
[2025-04-28 21:22:16,270 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 39 to 39.
[2025-04-28 21:22:16,270 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 39 states, 19 states have (on average 1.0526315789473684) internal successors, (20), 20 states have internal predecessors, (20), 3 states have call successors, (3), 2 states have call predecessors, (3), 16 states have return successors, (17), 16 states have call predecessors, (17), 3 states have call successors, (17)
[2025-04-28 21:22:16,270 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 39 states to 39 states and 40 transitions.
[2025-04-28 21:22:16,271 INFO  L79                 Accepts]: Start accepts. Automaton has 39 states and 40 transitions. Word has length 61
[2025-04-28 21:22:16,271 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:16,271 INFO  L485      AbstractCegarLoop]: Abstraction has 39 states and 40 transitions.
[2025-04-28 21:22:16,271 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 32 states, 16 states have (on average 2.0625) internal successors, (33), 31 states have internal predecessors, (33), 17 states have call successors, (17), 1 states have call predecessors, (17), 15 states have return successors, (29), 14 states have call predecessors, (29), 17 states have call successors, (29)
[2025-04-28 21:22:16,271 INFO  L278                IsEmpty]: Start isEmpty. Operand 39 states and 40 transitions.
[2025-04-28 21:22:16,272 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-04-28 21:22:16,272 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:16,272 INFO  L218           NwaCegarLoop]: trace histogram [15, 14, 14, 14, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:16,278 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (14)] Ended with exit code 0
[2025-04-28 21:22:16,473 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 14 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable14
[2025-04-28 21:22:16,473 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:16,473 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:16,473 INFO  L85        PathProgramCache]: Analyzing trace with hash -702996471, now seen corresponding path program 14 times
[2025-04-28 21:22:16,473 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:16,473 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [170083853]
[2025-04-28 21:22:16,473 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:16,474 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:16,479 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 65 statements into 2 equivalence classes.
[2025-04-28 21:22:16,492 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:22:16,492 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:16,492 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:16,895 INFO  L134       CoverageAnalysis]: Checked inductivity of 406 backedges. 0 proven. 210 refuted. 0 times theorem prover too weak. 196 trivial. 0 not checked.
[2025-04-28 21:22:16,896 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:16,896 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [170083853]
[2025-04-28 21:22:16,896 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [170083853] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:16,896 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1950745636]
[2025-04-28 21:22:16,896 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:16,896 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:16,898 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:16,901 INFO  L229       MonitoredProcess]: Starting monitored process 15 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:16,902 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Waiting until timeout for monitored process
[2025-04-28 21:22:16,987 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 65 statements into 2 equivalence classes.
[2025-04-28 21:22:17,005 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:22:17,005 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:17,005 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:17,008 INFO  L256         TraceCheckSpWp]: Trace formula consists of 129 conjuncts, 61 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:17,009 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:17,095 INFO  L134       CoverageAnalysis]: Checked inductivity of 406 backedges. 0 proven. 210 refuted. 0 times theorem prover too weak. 196 trivial. 0 not checked.
[2025-04-28 21:22:17,095 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:19,488 INFO  L134       CoverageAnalysis]: Checked inductivity of 406 backedges. 0 proven. 301 refuted. 0 times theorem prover too weak. 105 trivial. 0 not checked.
[2025-04-28 21:22:19,488 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1950745636] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:19,488 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:19,488 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [19, 19, 32] total 34
[2025-04-28 21:22:19,488 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1788143586]
[2025-04-28 21:22:19,488 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:19,489 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 34 states
[2025-04-28 21:22:19,489 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:19,490 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 34 interpolants.
[2025-04-28 21:22:19,490 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=94, Invalid=1028, Unknown=0, NotChecked=0, Total=1122
[2025-04-28 21:22:19,490 INFO  L87              Difference]: Start difference. First operand 39 states and 40 transitions. Second operand  has 34 states, 17 states have (on average 2.0588235294117645) internal successors, (35), 33 states have internal predecessors, (35), 18 states have call successors, (18), 1 states have call predecessors, (18), 16 states have return successors, (31), 15 states have call predecessors, (31), 18 states have call successors, (31)
[2025-04-28 21:22:20,016 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:20,016 INFO  L93              Difference]: Finished difference Result 41 states and 42 transitions.
[2025-04-28 21:22:20,017 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 19 states. 
[2025-04-28 21:22:20,017 INFO  L79                 Accepts]: Start accepts. Automaton has  has 34 states, 17 states have (on average 2.0588235294117645) internal successors, (35), 33 states have internal predecessors, (35), 18 states have call successors, (18), 1 states have call predecessors, (18), 16 states have return successors, (31), 15 states have call predecessors, (31), 18 states have call successors, (31) Word has length 65
[2025-04-28 21:22:20,017 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:20,018 INFO  L225             Difference]: With dead ends: 41
[2025-04-28 21:22:20,018 INFO  L226             Difference]: Without dead ends: 41
[2025-04-28 21:22:20,019 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 175 GetRequests, 128 SyntacticMatches, 1 SemanticMatches, 46 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 196 ImplicationChecksByTransitivity, 0.7s TimeCoverageRelationStatistics Valid=346, Invalid=1910, Unknown=0, NotChecked=0, Total=2256
[2025-04-28 21:22:20,019 INFO  L437           NwaCegarLoop]: 24 mSDtfsCounter, 199 mSDsluCounter, 366 mSDsCounter, 0 mSdLazyCounter, 357 mSolverCounterSat, 196 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 216 SdHoareTripleChecker+Valid, 390 SdHoareTripleChecker+Invalid, 553 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 196 IncrementalHoareTripleChecker+Valid, 357 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:20,020 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [216 Valid, 390 Invalid, 553 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [196 Valid, 357 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:20,020 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 41 states.
[2025-04-28 21:22:20,023 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 41 to 41.
[2025-04-28 21:22:20,024 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 41 states, 20 states have (on average 1.05) internal successors, (21), 21 states have internal predecessors, (21), 3 states have call successors, (3), 2 states have call predecessors, (3), 17 states have return successors, (18), 17 states have call predecessors, (18), 3 states have call successors, (18)
[2025-04-28 21:22:20,024 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 41 states to 41 states and 42 transitions.
[2025-04-28 21:22:20,024 INFO  L79                 Accepts]: Start accepts. Automaton has 41 states and 42 transitions. Word has length 65
[2025-04-28 21:22:20,025 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:20,025 INFO  L485      AbstractCegarLoop]: Abstraction has 41 states and 42 transitions.
[2025-04-28 21:22:20,025 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 34 states, 17 states have (on average 2.0588235294117645) internal successors, (35), 33 states have internal predecessors, (35), 18 states have call successors, (18), 1 states have call predecessors, (18), 16 states have return successors, (31), 15 states have call predecessors, (31), 18 states have call successors, (31)
[2025-04-28 21:22:20,025 INFO  L278                IsEmpty]: Start isEmpty. Operand 41 states and 42 transitions.
[2025-04-28 21:22:20,026 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 70
[2025-04-28 21:22:20,026 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:20,026 INFO  L218           NwaCegarLoop]: trace histogram [16, 15, 15, 15, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:20,033 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (15)] Ended with exit code 0
[2025-04-28 21:22:20,226 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 15 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-04-28 21:22:20,227 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:20,227 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:20,227 INFO  L85        PathProgramCache]: Analyzing trace with hash -735457461, now seen corresponding path program 15 times
[2025-04-28 21:22:20,227 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:20,227 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1772880832]
[2025-04-28 21:22:20,227 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:20,227 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:20,231 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 69 statements into 16 equivalence classes.
[2025-04-28 21:22:20,254 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 16 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:22:20,258 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 16 check-sat command(s)
[2025-04-28 21:22:20,258 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:20,737 INFO  L134       CoverageAnalysis]: Checked inductivity of 465 backedges. 0 proven. 240 refuted. 0 times theorem prover too weak. 225 trivial. 0 not checked.
[2025-04-28 21:22:20,737 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:20,737 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1772880832]
[2025-04-28 21:22:20,737 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1772880832] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:20,737 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1336290936]
[2025-04-28 21:22:20,738 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:22:20,738 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:20,740 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:20,742 INFO  L229       MonitoredProcess]: Starting monitored process 16 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:20,743 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (16)] Waiting until timeout for monitored process
[2025-04-28 21:22:20,843 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 69 statements into 16 equivalence classes.
[2025-04-28 21:22:20,865 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 16 check-sat command(s) and asserted 69 of 69 statements.
[2025-04-28 21:22:20,866 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 16 check-sat command(s)
[2025-04-28 21:22:20,866 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:20,867 INFO  L256         TraceCheckSpWp]: Trace formula consists of 137 conjuncts, 65 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:20,869 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:20,962 INFO  L134       CoverageAnalysis]: Checked inductivity of 465 backedges. 0 proven. 240 refuted. 0 times theorem prover too weak. 225 trivial. 0 not checked.
[2025-04-28 21:22:20,962 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
