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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:13,558 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:13,630 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d172180c-74e4-4cc5-a87c-9d1ba683626d/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:13,634 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:13,635 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:13,656 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:13,657 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:13,657 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:13,657 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:13,657 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:13,658 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:13,658 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:13,658 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:13,658 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:13,658 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:13,658 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:13,658 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:13,659 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:13,659 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:13,659 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:13,659 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:13,659 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:13,659 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:13,659 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:13,659 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:13,660 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:13,660 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:13,983 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:13,995 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:14,001 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:14,002 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:14,003 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:14,004 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d172180c-74e4-4cc5-a87c-9d1ba683626d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-270.smt2
[2025-04-28 21:21:14,008 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:14,013 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:14,190 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d172180c-74e4-4cc5-a87c-9d1ba683626d/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-270.smt2
[2025-04-28 21:21:14,194 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:14,197 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:14,198 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:14,198 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:14,198 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:14,205 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,237 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14 Unit
[2025-04-28 21:21:14,237 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:14,239 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,241 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:14,241 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:14,261 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,261 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,292 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,292 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,294 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,295 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,297 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,298 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,298 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,313 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,316 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:14,316 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:14,316 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:14,317 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,320 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:14,337 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:14,353 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:14,358 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:14,371 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:14,371 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:14,372 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:14,372 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fail given in one single declaration
[2025-04-28 21:21:14,372 INFO  L130     BoogieDeclarations]: Found specification of procedure fail
[2025-04-28 21:21:14,372 INFO  L138     BoogieDeclarations]: Found implementation of procedure fail
[2025-04-28 21:21:14,373 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:14,373 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:14,373 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:14,373 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:14,373 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:14,373 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:14,411 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:14,413 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:14,475 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:14,476 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:14,489 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:14,490 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:14,490 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14 BoogieIcfgContainer
[2025-04-28 21:21:14,491 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:14,496 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:14,496 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:14,503 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:14,503 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:14" (1/3) ...
[2025-04-28 21:21:14,504 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@568da876 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,504 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (2/3) ...
[2025-04-28 21:21:14,505 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@568da876 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,505 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14" (3/3) ...
[2025-04-28 21:21:14,506 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:14,525 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:14,530 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 16 locations, 21 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:14,592 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:14,616 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;@88db18f, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:14,616 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:14,624 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:14,634 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:14,634 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:14,635 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:14,636 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:14,644 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:14,644 INFO  L85        PathProgramCache]: Analyzing trace with hash 812378868, now seen corresponding path program 1 times
[2025-04-28 21:21:14,655 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:14,656 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [922782511]
[2025-04-28 21:21:14,656 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:14,657 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:14,694 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:14,719 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:14,720 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:14,720 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:14,819 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:14,820 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:14,820 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [922782511]
[2025-04-28 21:21:14,821 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [922782511] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:14,821 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:14,824 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:14,825 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1537310316]
[2025-04-28 21:21:14,826 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:14,830 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:14,830 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:14,870 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:14,870 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:14,872 INFO  L87              Difference]: Start difference. First operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:14,931 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:14,932 INFO  L93              Difference]: Finished difference Result 16 states and 17 transitions.
[2025-04-28 21:21:14,941 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:14,943 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:14,944 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:14,955 INFO  L225             Difference]: With dead ends: 16
[2025-04-28 21:21:14,955 INFO  L226             Difference]: Without dead ends: 16
[2025-04-28 21:21:14,958 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:14,963 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 1 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 35 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:14,964 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 35 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:14,983 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 16 states.
[2025-04-28 21:21:15,038 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 16 to 16.
[2025-04-28 21:21:15,039 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 16 states, 7 states have (on average 1.1428571428571428) internal successors, (8), 8 states have internal predecessors, (8), 4 states have call successors, (4), 3 states have call predecessors, (4), 4 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:15,046 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 16 states to 16 states and 17 transitions.
[2025-04-28 21:21:15,049 INFO  L79                 Accepts]: Start accepts. Automaton has 16 states and 17 transitions. Word has length 12
[2025-04-28 21:21:15,049 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:15,049 INFO  L485      AbstractCegarLoop]: Abstraction has 16 states and 17 transitions.
[2025-04-28 21:21:15,050 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:15,050 INFO  L278                IsEmpty]: Start isEmpty. Operand 16 states and 17 transitions.
[2025-04-28 21:21:15,053 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:15,054 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,054 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,055 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:15,055 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,056 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,056 INFO  L85        PathProgramCache]: Analyzing trace with hash 1337627512, now seen corresponding path program 1 times
[2025-04-28 21:21:15,056 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,056 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2102899260]
[2025-04-28 21:21:15,057 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,057 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,071 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:15,100 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:15,100 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,101 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,351 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:15,352 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:15,353 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2102899260]
[2025-04-28 21:21:15,353 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2102899260] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:15,354 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1959906901]
[2025-04-28 21:21:15,354 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,354 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:15,358 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:15,364 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:15,366 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:15,401 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:15,415 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:15,415 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,415 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:15,422 INFO  L256         TraceCheckSpWp]: Trace formula consists of 42 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:15,428 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:15,607 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:15,608 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:16,065 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:16,066 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1959906901] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:16,066 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:16,066 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:16,067 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [417186732]
[2025-04-28 21:21:16,067 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,067 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:16,068 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,068 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:16,069 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=38, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:16,069 INFO  L87              Difference]: Start difference. First operand 16 states and 17 transitions. Second operand  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:16,128 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,128 INFO  L93              Difference]: Finished difference Result 18 states and 19 transitions.
[2025-04-28 21:21:16,129 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:16,129 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6) Word has length 16
[2025-04-28 21:21:16,129 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,130 INFO  L225             Difference]: With dead ends: 18
[2025-04-28 21:21:16,130 INFO  L226             Difference]: Without dead ends: 18
[2025-04-28 21:21:16,130 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 27 SyntacticMatches, 4 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 8 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=23, Invalid=49, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:16,131 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 4 mSDsluCounter, 41 mSDsCounter, 0 mSdLazyCounter, 19 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 55 SdHoareTripleChecker+Invalid, 21 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 19 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,132 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 55 Invalid, 21 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 19 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:16,132 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 18 states.
[2025-04-28 21:21:16,135 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 18 to 18.
[2025-04-28 21:21:16,135 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 18 states, 8 states have (on average 1.125) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 5 states have return successors, (6), 5 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:16,136 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 18 states to 18 states and 19 transitions.
[2025-04-28 21:21:16,136 INFO  L79                 Accepts]: Start accepts. Automaton has 18 states and 19 transitions. Word has length 16
[2025-04-28 21:21:16,136 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,136 INFO  L485      AbstractCegarLoop]: Abstraction has 18 states and 19 transitions.
[2025-04-28 21:21:16,137 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:16,137 INFO  L278                IsEmpty]: Start isEmpty. Operand 18 states and 19 transitions.
[2025-04-28 21:21:16,137 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:16,137 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,138 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,146 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:16,343 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:16,343 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,344 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,344 INFO  L85        PathProgramCache]: Analyzing trace with hash 1410960252, now seen corresponding path program 2 times
[2025-04-28 21:21:16,344 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,344 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [42508665]
[2025-04-28 21:21:16,344 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:16,345 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,352 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:16,363 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:16,363 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:16,363 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,545 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:16,545 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,545 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [42508665]
[2025-04-28 21:21:16,545 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [42508665] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:16,545 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [717757210]
[2025-04-28 21:21:16,545 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:16,546 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:16,548 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:16,551 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:16,554 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:16,589 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:16,608 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:16,609 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:16,609 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,610 INFO  L256         TraceCheckSpWp]: Trace formula consists of 56 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:16,612 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:16,677 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:16,677 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:17,386 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:17,388 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [717757210] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:17,388 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:17,388 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 10
[2025-04-28 21:21:17,389 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [917841100]
[2025-04-28 21:21:17,389 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,389 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:17,389 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,390 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:17,392 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:17,393 INFO  L87              Difference]: Start difference. First operand 18 states and 19 transitions. Second operand  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:17,471 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,471 INFO  L93              Difference]: Finished difference Result 20 states and 21 transitions.
[2025-04-28 21:21:17,473 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:17,474 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8) Word has length 20
[2025-04-28 21:21:17,474 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,475 INFO  L225             Difference]: With dead ends: 20
[2025-04-28 21:21:17,475 INFO  L226             Difference]: Without dead ends: 20
[2025-04-28 21:21:17,475 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 34 SyntacticMatches, 5 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 20 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=42, Invalid=90, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:17,476 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 8 mSDsluCounter, 39 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 53 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,476 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 53 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:17,477 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 20 states.
[2025-04-28 21:21:17,480 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 20 to 20.
[2025-04-28 21:21:17,480 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 20 states, 9 states have (on average 1.1111111111111112) internal successors, (10), 10 states have internal predecessors, (10), 4 states have call successors, (4), 3 states have call predecessors, (4), 6 states have return successors, (7), 6 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:17,481 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 21 transitions.
[2025-04-28 21:21:17,481 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 21 transitions. Word has length 20
[2025-04-28 21:21:17,481 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,481 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 21 transitions.
[2025-04-28 21:21:17,482 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (8), 3 states have call predecessors, (8), 6 states have call successors, (8)
[2025-04-28 21:21:17,482 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 21 transitions.
[2025-04-28 21:21:17,482 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:17,482 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,483 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,488 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:17,687 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:17,687 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,688 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,688 INFO  L85        PathProgramCache]: Analyzing trace with hash -1097944320, now seen corresponding path program 3 times
[2025-04-28 21:21:17,688 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,688 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1892560877]
[2025-04-28 21:21:17,688 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:17,688 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,694 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:17,713 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:17,713 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:17,713 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,956 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:17,956 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,957 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1892560877]
[2025-04-28 21:21:17,957 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1892560877] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:17,957 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1150213868]
[2025-04-28 21:21:17,957 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:17,957 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:17,961 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:17,963 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:17,971 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:18,005 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:18,021 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:18,022 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:18,022 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,023 INFO  L256         TraceCheckSpWp]: Trace formula consists of 70 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:18,025 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:18,080 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:18,080 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:19,029 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:19,029 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1150213868] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:19,030 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:19,030 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 10] total 12
[2025-04-28 21:21:19,030 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1143691836]
[2025-04-28 21:21:19,030 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,030 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:19,030 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,031 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:19,031 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=92, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:19,032 INFO  L87              Difference]: Start difference. First operand 20 states and 21 transitions. Second operand  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:19,117 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,117 INFO  L93              Difference]: Finished difference Result 22 states and 23 transitions.
[2025-04-28 21:21:19,118 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:19,118 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10) Word has length 24
[2025-04-28 21:21:19,119 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,119 INFO  L225             Difference]: With dead ends: 22
[2025-04-28 21:21:19,119 INFO  L226             Difference]: Without dead ends: 22
[2025-04-28 21:21:19,120 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 60 GetRequests, 41 SyntacticMatches, 6 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 38 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=67, Invalid=143, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:19,120 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 6 mSDsluCounter, 64 mSDsCounter, 0 mSdLazyCounter, 33 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 78 SdHoareTripleChecker+Invalid, 34 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 33 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,121 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 78 Invalid, 34 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 33 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:19,121 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 22 states.
[2025-04-28 21:21:19,125 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 22 to 22.
[2025-04-28 21:21:19,125 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 10 states have (on average 1.1) internal successors, (11), 11 states have internal predecessors, (11), 4 states have call successors, (4), 3 states have call predecessors, (4), 7 states have return successors, (8), 7 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:21:19,126 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 23 transitions.
[2025-04-28 21:21:19,127 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 23 transitions. Word has length 24
[2025-04-28 21:21:19,127 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,127 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 23 transitions.
[2025-04-28 21:21:19,128 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 11 states have internal predecessors, (14), 7 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (10), 4 states have call predecessors, (10), 7 states have call successors, (10)
[2025-04-28 21:21:19,128 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 23 transitions.
[2025-04-28 21:21:19,129 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:19,129 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,129 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,135 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:19,330 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:19,330 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,331 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,331 INFO  L85        PathProgramCache]: Analyzing trace with hash 306702852, now seen corresponding path program 4 times
[2025-04-28 21:21:19,331 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,331 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1022562712]
[2025-04-28 21:21:19,332 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:19,332 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,338 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:19,381 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:19,381 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:19,381 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,647 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:19,648 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,649 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1022562712]
[2025-04-28 21:21:19,649 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1022562712] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:19,649 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1868798070]
[2025-04-28 21:21:19,649 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:19,649 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:19,652 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:19,654 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:19,658 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:19,699 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:19,719 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:19,719 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:19,719 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,722 INFO  L256         TraceCheckSpWp]: Trace formula consists of 84 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:19,724 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:19,776 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:19,777 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:21,197 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:21,197 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1868798070] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:21,197 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:21,197 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 12] total 15
[2025-04-28 21:21:21,197 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [151781538]
[2025-04-28 21:21:21,198 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,198 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:21,198 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,199 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:21,199 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=61, Invalid=149, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:21,200 INFO  L87              Difference]: Start difference. First operand 22 states and 23 transitions. Second operand  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (13), 5 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:21,319 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,319 INFO  L93              Difference]: Finished difference Result 24 states and 25 transitions.
[2025-04-28 21:21:21,320 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:21,320 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (13), 5 states have call predecessors, (13), 9 states have call successors, (13) Word has length 28
[2025-04-28 21:21:21,320 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,321 INFO  L225             Difference]: With dead ends: 24
[2025-04-28 21:21:21,321 INFO  L226             Difference]: Without dead ends: 24
[2025-04-28 21:21:21,321 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 71 GetRequests, 47 SyntacticMatches, 7 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 74 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=109, Invalid=233, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:21,322 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 15 mSDsluCounter, 76 mSDsCounter, 0 mSdLazyCounter, 36 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 90 SdHoareTripleChecker+Invalid, 47 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 36 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,323 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 90 Invalid, 47 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 36 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:21,323 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 24 states.
[2025-04-28 21:21:21,326 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 24 to 24.
[2025-04-28 21:21:21,327 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 4 states have call successors, (4), 3 states have call predecessors, (4), 8 states have return successors, (9), 8 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:21,327 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 25 transitions.
[2025-04-28 21:21:21,328 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 25 transitions. Word has length 28
[2025-04-28 21:21:21,328 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,328 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 25 transitions.
[2025-04-28 21:21:21,328 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (13), 5 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:21,328 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 25 transitions.
[2025-04-28 21:21:21,329 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:21,329 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,329 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,335 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:21,533 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:21,534 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,534 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,535 INFO  L85        PathProgramCache]: Analyzing trace with hash -627371896, now seen corresponding path program 5 times
[2025-04-28 21:21:21,535 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,535 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [543214372]
[2025-04-28 21:21:21,535 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:21,535 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,545 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 32 statements into 6 equivalence classes.
[2025-04-28 21:21:21,605 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:21,605 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:21,605 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,823 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:21,823 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,823 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [543214372]
[2025-04-28 21:21:21,823 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [543214372] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:21,823 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [630686270]
[2025-04-28 21:21:21,824 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:21,824 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:21,826 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:21,828 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:21,832 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:21,883 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 32 statements into 6 equivalence classes.
[2025-04-28 21:21:21,906 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:21,907 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:21,907 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,908 INFO  L256         TraceCheckSpWp]: Trace formula consists of 98 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:21,909 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:21,966 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:21,966 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:24,045 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:24,045 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [630686270] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:24,045 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:24,045 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 14] total 16
[2025-04-28 21:21:24,046 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1680585675]
[2025-04-28 21:21:24,046 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:24,046 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:24,046 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:24,047 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:24,047 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=70, Invalid=170, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:24,048 INFO  L87              Difference]: Start difference. First operand 24 states and 25 transitions. Second operand  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (14), 6 states have call predecessors, (14), 9 states have call successors, (14)
[2025-04-28 21:21:24,179 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:24,179 INFO  L93              Difference]: Finished difference Result 26 states and 27 transitions.
[2025-04-28 21:21:24,179 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:24,180 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (14), 6 states have call predecessors, (14), 9 states have call successors, (14) Word has length 32
[2025-04-28 21:21:24,180 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:24,181 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:24,183 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:24,184 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 82 GetRequests, 55 SyntacticMatches, 8 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 92 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=135, Invalid=285, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:24,185 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 15 mSDsluCounter, 66 mSDsCounter, 0 mSdLazyCounter, 36 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 80 SdHoareTripleChecker+Invalid, 47 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 36 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:24,185 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 80 Invalid, 47 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 36 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:24,186 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:24,188 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:24,191 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.0833333333333333) internal successors, (13), 13 states have internal predecessors, (13), 4 states have call successors, (4), 3 states have call predecessors, (4), 9 states have return successors, (10), 9 states have call predecessors, (10), 4 states have call successors, (10)
[2025-04-28 21:21:24,192 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 27 transitions.
[2025-04-28 21:21:24,192 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 27 transitions. Word has length 32
[2025-04-28 21:21:24,193 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:24,193 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 27 transitions.
[2025-04-28 21:21:24,193 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (14), 6 states have call predecessors, (14), 9 states have call successors, (14)
[2025-04-28 21:21:24,193 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 27 transitions.
[2025-04-28 21:21:24,194 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:24,194 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,194 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:24,199 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:24,395 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:24,395 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,396 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,396 INFO  L85        PathProgramCache]: Analyzing trace with hash 822478476, now seen corresponding path program 6 times
[2025-04-28 21:21:24,396 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,396 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [840574124]
[2025-04-28 21:21:24,396 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:24,396 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,404 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:24,447 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:24,448 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:24,448 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,724 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 3 proven. 44 refuted. 0 times theorem prover too weak. 31 trivial. 0 not checked.
[2025-04-28 21:21:24,724 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,725 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [840574124]
[2025-04-28 21:21:24,725 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [840574124] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:24,725 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1034632769]
[2025-04-28 21:21:24,725 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:24,725 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:24,728 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:24,730 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:24,733 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:24,801 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:24,837 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:21:24,837 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:24,837 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,839 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:24,841 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:24,916 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:24,916 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:27,780 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:27,780 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1034632769] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:27,780 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:27,781 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 16] total 19
[2025-04-28 21:21:27,781 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [276352020]
[2025-04-28 21:21:27,781 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,781 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:27,781 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,782 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:27,782 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=97, Invalid=245, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:27,783 INFO  L87              Difference]: Start difference. First operand 26 states and 27 transitions. Second operand  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (17), 7 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:27,928 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,928 INFO  L93              Difference]: Finished difference Result 28 states and 29 transitions.
[2025-04-28 21:21:27,929 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:27,930 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (17), 7 states have call predecessors, (17), 11 states have call successors, (17) Word has length 36
[2025-04-28 21:21:27,930 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,930 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:27,931 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:27,931 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 93 GetRequests, 61 SyntacticMatches, 9 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 156 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=193, Invalid=407, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:27,932 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 26 mSDsluCounter, 76 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 35 SdHoareTripleChecker+Valid, 90 SdHoareTripleChecker+Invalid, 63 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,932 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [35 Valid, 90 Invalid, 63 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:27,933 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:27,936 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 28.
[2025-04-28 21:21:27,936 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 4 states have call successors, (4), 3 states have call predecessors, (4), 10 states have return successors, (11), 10 states have call predecessors, (11), 4 states have call successors, (11)
[2025-04-28 21:21:27,937 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 29 transitions.
[2025-04-28 21:21:27,937 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 29 transitions. Word has length 36
[2025-04-28 21:21:27,937 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,937 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 29 transitions.
[2025-04-28 21:21:27,937 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (17), 7 states have call predecessors, (17), 11 states have call successors, (17)
[2025-04-28 21:21:27,937 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 29 transitions.
[2025-04-28 21:21:27,938 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:27,938 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,938 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,942 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:28,139 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:28,139 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:28,139 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:28,139 INFO  L85        PathProgramCache]: Analyzing trace with hash -1020351472, now seen corresponding path program 7 times
[2025-04-28 21:21:28,140 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:28,140 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [988472515]
[2025-04-28 21:21:28,140 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:28,140 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:28,145 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:28,153 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:28,153 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,153 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,403 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:28,403 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,403 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [988472515]
[2025-04-28 21:21:28,403 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [988472515] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,403 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1394932080]
[2025-04-28 21:21:28,403 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:28,403 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,406 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,409 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:28,413 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,528 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:28,550 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:28,550 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,550 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,551 INFO  L256         TraceCheckSpWp]: Trace formula consists of 126 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,553 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,628 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:28,629 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:32,235 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:32,236 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1394932080] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:32,236 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:32,236 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 18] total 20
[2025-04-28 21:21:32,236 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1010311931]
[2025-04-28 21:21:32,236 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,237 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:32,237 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,237 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:32,238 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=108, Invalid=272, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:32,238 INFO  L87              Difference]: Start difference. First operand 28 states and 29 transitions. Second operand  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (18), 8 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:21:32,374 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,374 INFO  L93              Difference]: Finished difference Result 30 states and 31 transitions.
[2025-04-28 21:21:32,376 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:32,377 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (18), 8 states have call predecessors, (18), 11 states have call successors, (18) Word has length 40
[2025-04-28 21:21:32,377 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,379 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:32,381 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:32,382 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 104 GetRequests, 69 SyntacticMatches, 10 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 170 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=227, Invalid=475, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:32,382 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 16 mSDsluCounter, 95 mSDsCounter, 0 mSdLazyCounter, 48 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 109 SdHoareTripleChecker+Invalid, 58 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 48 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,383 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 109 Invalid, 58 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 48 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:32,383 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:32,388 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 30.
[2025-04-28 21:21:32,389 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 30 states, 14 states have (on average 1.0714285714285714) internal successors, (15), 15 states have internal predecessors, (15), 4 states have call successors, (4), 3 states have call predecessors, (4), 11 states have return successors, (12), 11 states have call predecessors, (12), 4 states have call successors, (12)
[2025-04-28 21:21:32,389 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 31 transitions.
[2025-04-28 21:21:32,390 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 31 transitions. Word has length 40
[2025-04-28 21:21:32,390 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,390 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 31 transitions.
[2025-04-28 21:21:32,390 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 10 states have (on average 2.2) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (18), 8 states have call predecessors, (18), 11 states have call successors, (18)
[2025-04-28 21:21:32,390 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 31 transitions.
[2025-04-28 21:21:32,391 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:32,391 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,391 INFO  L218           NwaCegarLoop]: trace histogram [9, 8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,396 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:32,594 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable8
[2025-04-28 21:21:32,594 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,595 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,595 INFO  L85        PathProgramCache]: Analyzing trace with hash 1491263764, now seen corresponding path program 8 times
[2025-04-28 21:21:32,595 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,595 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1065854408]
[2025-04-28 21:21:32,595 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:32,596 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,602 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 44 statements into 2 equivalence classes.
[2025-04-28 21:21:32,612 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:32,612 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:32,612 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,892 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:21:32,892 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,892 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1065854408]
[2025-04-28 21:21:32,892 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1065854408] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:32,893 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [35489831]
[2025-04-28 21:21:32,893 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:32,893 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,895 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:32,897 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:32,901 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,045 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 44 statements into 2 equivalence classes.
[2025-04-28 21:21:33,068 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:33,068 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:33,068 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,070 INFO  L256         TraceCheckSpWp]: Trace formula consists of 140 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,072 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,136 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:21:33,136 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:37,993 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:21:37,993 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [35489831] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:37,993 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:37,993 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 13, 20] total 22
[2025-04-28 21:21:37,993 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1156278875]
[2025-04-28 21:21:37,993 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,994 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 22 states
[2025-04-28 21:21:37,994 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,994 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 22 interpolants.
[2025-04-28 21:21:37,995 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=130, Invalid=332, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:37,995 INFO  L87              Difference]: Start difference. First operand 30 states and 31 transitions. Second operand  has 22 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 21 states have internal predecessors, (24), 12 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 12 states have call successors, (20)
[2025-04-28 21:21:38,157 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,157 INFO  L93              Difference]: Finished difference Result 32 states and 33 transitions.
[2025-04-28 21:21:38,158 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:38,158 INFO  L79                 Accepts]: Start accepts. Automaton has  has 22 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 21 states have internal predecessors, (24), 12 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 12 states have call successors, (20) Word has length 44
[2025-04-28 21:21:38,158 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,159 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:38,159 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:38,163 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 115 GetRequests, 76 SyntacticMatches, 11 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 218 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=282, Invalid=588, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:38,164 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 38 mSDsluCounter, 96 mSDsCounter, 0 mSdLazyCounter, 46 mSolverCounterSat, 35 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 49 SdHoareTripleChecker+Valid, 110 SdHoareTripleChecker+Invalid, 81 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 35 IncrementalHoareTripleChecker+Valid, 46 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,166 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [49 Valid, 110 Invalid, 81 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [35 Valid, 46 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:38,166 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:38,172 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:21:38,176 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 15 states have (on average 1.0666666666666667) internal successors, (16), 16 states have internal predecessors, (16), 4 states have call successors, (4), 3 states have call predecessors, (4), 12 states have return successors, (13), 12 states have call predecessors, (13), 4 states have call successors, (13)
[2025-04-28 21:21:38,177 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 33 transitions.
[2025-04-28 21:21:38,177 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 33 transitions. Word has length 44
[2025-04-28 21:21:38,177 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,177 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 33 transitions.
[2025-04-28 21:21:38,177 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 22 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 21 states have internal predecessors, (24), 12 states have call successors, (13), 1 states have call predecessors, (13), 10 states have return successors, (20), 9 states have call predecessors, (20), 12 states have call successors, (20)
[2025-04-28 21:21:38,177 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 33 transitions.
[2025-04-28 21:21:38,178 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:21:38,178 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,178 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,184 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:38,379 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:21:38,379 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,379 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,379 INFO  L85        PathProgramCache]: Analyzing trace with hash -635927144, now seen corresponding path program 9 times
[2025-04-28 21:21:38,380 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,380 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [797002943]
[2025-04-28 21:21:38,380 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:38,380 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,388 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 10 equivalence classes.
[2025-04-28 21:21:38,476 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:38,477 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:38,477 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,070 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 2 proven. 108 refuted. 0 times theorem prover too weak. 61 trivial. 0 not checked.
[2025-04-28 21:21:39,071 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,071 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [797002943]
[2025-04-28 21:21:39,071 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [797002943] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,071 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1542334214]
[2025-04-28 21:21:39,071 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:39,071 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,073 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,076 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:21:39,079 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,319 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 10 equivalence classes.
[2025-04-28 21:21:39,385 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:39,386 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:39,386 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,387 INFO  L256         TraceCheckSpWp]: Trace formula consists of 154 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,389 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,517 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:21:39,519 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,546 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:21:46,546 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1542334214] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,546 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,547 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [16, 14, 22] total 26
[2025-04-28 21:21:46,547 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1366667079]
[2025-04-28 21:21:46,547 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,547 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:46,547 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,548 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:46,548 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=179, Invalid=471, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:46,549 INFO  L87              Difference]: Start difference. First operand 32 states and 33 transitions. Second operand  has 26 states, 12 states have (on average 2.3333333333333335) internal successors, (28), 25 states have internal predecessors, (28), 15 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (25), 10 states have call predecessors, (25), 15 states have call successors, (25)
[2025-04-28 21:21:46,718 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,718 INFO  L93              Difference]: Finished difference Result 34 states and 35 transitions.
[2025-04-28 21:21:46,719 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:46,719 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 12 states have (on average 2.3333333333333335) internal successors, (28), 25 states have internal predecessors, (28), 15 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (25), 10 states have call predecessors, (25), 15 states have call successors, (25) Word has length 48
[2025-04-28 21:21:46,719 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,720 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:46,720 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:46,720 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 126 GetRequests, 81 SyntacticMatches, 12 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 328 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=386, Invalid=804, Unknown=0, NotChecked=0, Total=1190
[2025-04-28 21:21:46,721 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 17 mSDsluCounter, 96 mSDsCounter, 0 mSdLazyCounter, 50 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 110 SdHoareTripleChecker+Invalid, 57 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 50 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,721 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 110 Invalid, 57 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 50 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:46,722 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:46,724 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 34.
[2025-04-28 21:21:46,725 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 16 states have (on average 1.0625) internal successors, (17), 17 states have internal predecessors, (17), 4 states have call successors, (4), 3 states have call predecessors, (4), 13 states have return successors, (14), 13 states have call predecessors, (14), 4 states have call successors, (14)
[2025-04-28 21:21:46,725 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 35 transitions.
[2025-04-28 21:21:46,725 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 35 transitions. Word has length 48
[2025-04-28 21:21:46,725 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,725 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 35 transitions.
[2025-04-28 21:21:46,726 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 12 states have (on average 2.3333333333333335) internal successors, (28), 25 states have internal predecessors, (28), 15 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (25), 10 states have call predecessors, (25), 15 states have call successors, (25)
[2025-04-28 21:21:46,726 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 35 transitions.
[2025-04-28 21:21:46,726 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:46,727 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,727 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,732 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Ended with exit code 0
[2025-04-28 21:21:46,931 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:21:46,931 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,932 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,932 INFO  L85        PathProgramCache]: Analyzing trace with hash -722634340, now seen corresponding path program 10 times
[2025-04-28 21:21:46,932 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,932 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1600592035]
[2025-04-28 21:21:46,932 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:46,932 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,941 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 52 statements into 2 equivalence classes.
[2025-04-28 21:21:46,981 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:46,981 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:46,981 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,385 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:21:47,385 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,385 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1600592035]
[2025-04-28 21:21:47,385 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1600592035] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,385 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2039169248]
[2025-04-28 21:21:47,386 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:47,386 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,388 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,390 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:21:47,393 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,686 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 52 statements into 2 equivalence classes.
[2025-04-28 21:21:47,718 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:47,718 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:47,718 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,720 INFO  L256         TraceCheckSpWp]: Trace formula consists of 168 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,722 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,791 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:21:47,791 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
