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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:14,866 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:14,987 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f700cda1-f9ee-486a-b44a-fe8bae25472f/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:14,994 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:14,998 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:15,040 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:15,040 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:15,041 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:15,041 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:15,041 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:15,041 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:15,042 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:15,042 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:15,042 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:15,044 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:15,045 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:15,045 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:15,045 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:15,045 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:15,045 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:15,045 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:15,045 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:15,045 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:15,046 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:15,046 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:15,047 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:15,047 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:15,426 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:15,440 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:15,444 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:15,448 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:15,449 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:15,450 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f700cda1-f9ee-486a-b44a-fe8bae25472f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-275.smt2
[2025-04-28 21:21:15,454 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:15,458 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:15,638 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f700cda1-f9ee-486a-b44a-fe8bae25472f/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-275.smt2
[2025-04-28 21:21:15,642 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:15,644 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:15,645 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:15,645 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:15,645 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:15,649 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,683 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15 Unit
[2025-04-28 21:21:15,683 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:15,685 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,685 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:15,685 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:15,705 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,705 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,737 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,737 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,739 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,740 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,742 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,744 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,745 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,762 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,765 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:15,766 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:15,766 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:15,767 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,771 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:15,790 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:15,809 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:15,813 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:15,833 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:15,834 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:15,834 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:15,834 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fail given in one single declaration
[2025-04-28 21:21:15,834 INFO  L130     BoogieDeclarations]: Found specification of procedure fail
[2025-04-28 21:21:15,834 INFO  L138     BoogieDeclarations]: Found implementation of procedure fail
[2025-04-28 21:21:15,834 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:15,835 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:15,835 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:15,835 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:15,835 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:15,835 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:15,888 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:15,891 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:15,962 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:15,962 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:15,975 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:15,976 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:15,976 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:15 BoogieIcfgContainer
[2025-04-28 21:21:15,976 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:15,979 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:15,980 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:15,984 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:15,985 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/3) ...
[2025-04-28 21:21:15,986 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@84e1f56 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:15, skipping insertion in model container
[2025-04-28 21:21:15,986 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (2/3) ...
[2025-04-28 21:21:15,986 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@84e1f56 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:15, skipping insertion in model container
[2025-04-28 21:21:15,986 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:15" (3/3) ...
[2025-04-28 21:21:15,988 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:16,008 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:16,012 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:16,069 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:16,093 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;@315948d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:16,094 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:16,099 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:16,110 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:16,110 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,111 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,111 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,119 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,120 INFO  L85        PathProgramCache]: Analyzing trace with hash -121084841, now seen corresponding path program 1 times
[2025-04-28 21:21:16,131 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,131 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1854173296]
[2025-04-28 21:21:16,132 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,132 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,176 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:16,199 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:16,201 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,202 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,333 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:16,336 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,336 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1854173296]
[2025-04-28 21:21:16,337 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1854173296] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,337 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,342 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:16,344 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1905351426]
[2025-04-28 21:21:16,345 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,350 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:16,351 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,395 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:16,396 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:16,398 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:16,445 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,446 INFO  L93              Difference]: Finished difference Result 16 states and 17 transitions.
[2025-04-28 21:21:16,448 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:16,449 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:16,450 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,458 INFO  L225             Difference]: With dead ends: 16
[2025-04-28 21:21:16,458 INFO  L226             Difference]: Without dead ends: 16
[2025-04-28 21:21:16,461 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:16,465 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:16,466 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:16,488 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 16 states.
[2025-04-28 21:21:16,525 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 16 to 16.
[2025-04-28 21:21:16,527 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:16,532 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 16 states to 16 states and 17 transitions.
[2025-04-28 21:21:16,533 INFO  L79                 Accepts]: Start accepts. Automaton has 16 states and 17 transitions. Word has length 12
[2025-04-28 21:21:16,534 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,534 INFO  L485      AbstractCegarLoop]: Abstraction has 16 states and 17 transitions.
[2025-04-28 21:21:16,534 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:16,534 INFO  L278                IsEmpty]: Start isEmpty. Operand 16 states and 17 transitions.
[2025-04-28 21:21:16,536 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:16,536 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,536 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:16,537 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:16,537 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,538 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,538 INFO  L85        PathProgramCache]: Analyzing trace with hash -2109633831, now seen corresponding path program 1 times
[2025-04-28 21:21:16,538 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,538 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [837045774]
[2025-04-28 21:21:16,538 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,538 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,544 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:16,561 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:16,561 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,561 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,853 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,857 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,857 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [837045774]
[2025-04-28 21:21:16,857 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [837045774] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:16,858 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [563727047]
[2025-04-28 21:21:16,858 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,858 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:16,861 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:16,864 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:16,868 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:16,961 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:16,976 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:16,976 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,977 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,979 INFO  L256         TraceCheckSpWp]: Trace formula consists of 32 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:16,985 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:17,263 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:17,265 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:17,623 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:17,624 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [563727047] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:17,624 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:17,624 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:17,625 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1083254693]
[2025-04-28 21:21:17,625 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,626 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:17,626 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,628 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:17,629 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=61, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:17,630 INFO  L87              Difference]: Start difference. First operand 16 states and 17 transitions. Second operand  has 10 states, 5 states have (on average 2.6) internal successors, (13), 9 states have internal predecessors, (13), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 2 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:17,743 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,746 INFO  L93              Difference]: Finished difference Result 18 states and 19 transitions.
[2025-04-28 21:21:17,747 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:17,747 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.6) internal successors, (13), 9 states have internal predecessors, (13), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 2 states have call predecessors, (7), 6 states have call successors, (7) Word has length 16
[2025-04-28 21:21:17,747 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,748 INFO  L225             Difference]: With dead ends: 18
[2025-04-28 21:21:17,748 INFO  L226             Difference]: Without dead ends: 18
[2025-04-28 21:21:17,748 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 38 GetRequests, 27 SyntacticMatches, 2 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 20 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=35, Invalid=75, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:17,749 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 3 mSDsluCounter, 58 mSDsCounter, 0 mSdLazyCounter, 26 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 72 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 26 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,750 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 72 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 26 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:17,752 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 18 states.
[2025-04-28 21:21:17,758 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 18 to 18.
[2025-04-28 21:21:17,760 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:17,761 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 18 states to 18 states and 19 transitions.
[2025-04-28 21:21:17,762 INFO  L79                 Accepts]: Start accepts. Automaton has 18 states and 19 transitions. Word has length 16
[2025-04-28 21:21:17,762 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,762 INFO  L485      AbstractCegarLoop]: Abstraction has 18 states and 19 transitions.
[2025-04-28 21:21:17,763 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.6) internal successors, (13), 9 states have internal predecessors, (13), 6 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 2 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:17,763 INFO  L278                IsEmpty]: Start isEmpty. Operand 18 states and 19 transitions.
[2025-04-28 21:21:17,765 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:17,765 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,765 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:17,772 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:17,966 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:17,966 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,967 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,968 INFO  L85        PathProgramCache]: Analyzing trace with hash -1008473509, now seen corresponding path program 2 times
[2025-04-28 21:21:17,969 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,969 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [695481784]
[2025-04-28 21:21:17,969 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:17,969 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,981 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:18,003 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:18,003 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:18,003 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,381 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:18,382 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,382 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [695481784]
[2025-04-28 21:21:18,382 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [695481784] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:18,382 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1841863565]
[2025-04-28 21:21:18,382 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:18,382 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:18,386 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:18,388 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:18,391 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:18,425 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 20 statements into 2 equivalence classes.
[2025-04-28 21:21:18,441 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:18,442 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:18,442 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,443 INFO  L256         TraceCheckSpWp]: Trace formula consists of 40 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:18,444 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:18,624 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:18,625 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:19,191 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:19,192 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1841863565] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:19,192 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:19,192 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 13
[2025-04-28 21:21:19,192 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1898207980]
[2025-04-28 21:21:19,192 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,193 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:19,193 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,194 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:19,194 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=110, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:19,194 INFO  L87              Difference]: Start difference. First operand 18 states and 19 transitions. Second operand  has 13 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 12 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (11), 3 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:19,334 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,334 INFO  L93              Difference]: Finished difference Result 20 states and 21 transitions.
[2025-04-28 21:21:19,338 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:19,339 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 12 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (11), 3 states have call predecessors, (11), 8 states have call successors, (11) Word has length 20
[2025-04-28 21:21:19,339 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,339 INFO  L225             Difference]: With dead ends: 20
[2025-04-28 21:21:19,340 INFO  L226             Difference]: Without dead ends: 20
[2025-04-28 21:21:19,340 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 49 GetRequests, 34 SyntacticMatches, 2 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 49 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=62, Invalid=148, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:19,341 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 8 mSDsluCounter, 61 mSDsCounter, 0 mSdLazyCounter, 27 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 75 SdHoareTripleChecker+Invalid, 33 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 27 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,341 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 75 Invalid, 33 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 27 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:19,344 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 20 states.
[2025-04-28 21:21:19,350 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 20 to 20.
[2025-04-28 21:21:19,351 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:19,351 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 21 transitions.
[2025-04-28 21:21:19,351 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 21 transitions. Word has length 20
[2025-04-28 21:21:19,352 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,352 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 21 transitions.
[2025-04-28 21:21:19,352 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 12 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (11), 3 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:19,352 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 21 transitions.
[2025-04-28 21:21:19,353 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:19,353 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,353 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:19,359 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:19,554 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:19,554 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,554 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,554 INFO  L85        PathProgramCache]: Analyzing trace with hash 880837341, now seen corresponding path program 3 times
[2025-04-28 21:21:19,555 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,555 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2040121134]
[2025-04-28 21:21:19,555 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:19,555 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,564 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:19,574 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:19,575 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:19,575 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,089 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 1 proven. 14 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:20,090 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,090 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2040121134]
[2025-04-28 21:21:20,090 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2040121134] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:20,090 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1268811103]
[2025-04-28 21:21:20,090 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:20,090 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:20,095 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:20,097 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:20,102 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:20,138 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 24 statements into 4 equivalence classes.
[2025-04-28 21:21:20,157 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:20,158 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:20,158 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,160 INFO  L256         TraceCheckSpWp]: Trace formula consists of 48 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:20,163 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:20,385 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:20,388 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:21,822 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:21,822 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1268811103] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:21,823 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:21,823 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 8, 10] total 15
[2025-04-28 21:21:21,823 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1591110004]
[2025-04-28 21:21:21,823 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,824 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:21,824 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,826 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:21,826 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=58, Invalid=152, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:21,827 INFO  L87              Difference]: Start difference. First operand 20 states and 21 transitions. Second operand  has 15 states, 6 states have (on average 2.8333333333333335) internal successors, (17), 14 states have internal predecessors, (17), 10 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (13), 4 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:22,105 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:22,105 INFO  L93              Difference]: Finished difference Result 22 states and 23 transitions.
[2025-04-28 21:21:22,105 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:22,106 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 6 states have (on average 2.8333333333333335) internal successors, (17), 14 states have internal predecessors, (17), 10 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (13), 4 states have call predecessors, (13), 10 states have call successors, (13) Word has length 24
[2025-04-28 21:21:22,106 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:22,107 INFO  L225             Difference]: With dead ends: 22
[2025-04-28 21:21:22,107 INFO  L226             Difference]: Without dead ends: 22
[2025-04-28 21:21:22,107 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 61 GetRequests, 39 SyntacticMatches, 5 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 77 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=106, Invalid=236, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:22,108 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 14 mSDsluCounter, 57 mSDsCounter, 0 mSdLazyCounter, 30 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 71 SdHoareTripleChecker+Invalid, 46 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 30 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:22,109 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 71 Invalid, 46 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 30 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:22,109 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 22 states.
[2025-04-28 21:21:22,112 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 22 to 22.
[2025-04-28 21:21:22,113 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:22,113 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 23 transitions.
[2025-04-28 21:21:22,114 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 23 transitions. Word has length 24
[2025-04-28 21:21:22,114 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:22,114 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 23 transitions.
[2025-04-28 21:21:22,114 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 6 states have (on average 2.8333333333333335) internal successors, (17), 14 states have internal predecessors, (17), 10 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (13), 4 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:22,114 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 23 transitions.
[2025-04-28 21:21:22,115 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:22,115 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,115 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:22,122 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:22,316 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:22,316 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,317 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,317 INFO  L85        PathProgramCache]: Analyzing trace with hash -888646561, now seen corresponding path program 4 times
[2025-04-28 21:21:22,317 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,317 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [914000315]
[2025-04-28 21:21:22,317 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:22,318 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,324 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:22,333 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:22,333 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:22,333 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,614 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:22,614 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,615 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [914000315]
[2025-04-28 21:21:22,615 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [914000315] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:22,615 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [117053328]
[2025-04-28 21:21:22,615 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:22,615 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:22,618 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,620 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:22,624 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:22,673 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:22,684 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:22,684 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:22,685 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,686 INFO  L256         TraceCheckSpWp]: Trace formula consists of 56 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:22,687 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:22,840 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:22,842 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:25,063 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:25,063 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [117053328] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:25,063 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:25,064 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 12] total 17
[2025-04-28 21:21:25,064 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1354326331]
[2025-04-28 21:21:25,064 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,064 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:25,064 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,065 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:25,065 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=74, Invalid=198, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:25,067 INFO  L87              Difference]: Start difference. First operand 22 states and 23 transitions. Second operand  has 17 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (16), 5 states have call predecessors, (16), 10 states have call successors, (16)
[2025-04-28 21:21:25,327 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,327 INFO  L93              Difference]: Finished difference Result 24 states and 25 transitions.
[2025-04-28 21:21:25,328 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:25,328 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (16), 5 states have call predecessors, (16), 10 states have call successors, (16) Word has length 28
[2025-04-28 21:21:25,329 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,329 INFO  L225             Difference]: With dead ends: 24
[2025-04-28 21:21:25,329 INFO  L226             Difference]: Without dead ends: 24
[2025-04-28 21:21:25,332 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 72 GetRequests, 46 SyntacticMatches, 6 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 104 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=139, Invalid=323, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:25,334 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 23 mSDsluCounter, 75 mSDsCounter, 0 mSdLazyCounter, 38 mSolverCounterSat, 27 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 89 SdHoareTripleChecker+Invalid, 65 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 27 IncrementalHoareTripleChecker+Valid, 38 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:25,337 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 89 Invalid, 65 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [27 Valid, 38 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:25,338 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 24 states.
[2025-04-28 21:21:25,341 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 24 to 24.
[2025-04-28 21:21:25,345 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:25,346 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 25 transitions.
[2025-04-28 21:21:25,348 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 25 transitions. Word has length 28
[2025-04-28 21:21:25,349 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,349 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 25 transitions.
[2025-04-28 21:21:25,349 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 8 states have (on average 2.5) internal successors, (20), 16 states have internal predecessors, (20), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (16), 5 states have call predecessors, (16), 10 states have call successors, (16)
[2025-04-28 21:21:25,349 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 25 transitions.
[2025-04-28 21:21:25,350 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:25,350 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,350 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:25,355 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:25,551 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:25,551 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,552 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,552 INFO  L85        PathProgramCache]: Analyzing trace with hash 1183604449, now seen corresponding path program 5 times
[2025-04-28 21:21:25,552 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,552 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [12003644]
[2025-04-28 21:21:25,552 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:25,552 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,560 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 32 statements into 6 equivalence classes.
[2025-04-28 21:21:25,583 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:25,586 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:25,586 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,949 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 36 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:25,949 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,949 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [12003644]
[2025-04-28 21:21:25,950 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [12003644] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:25,950 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1715899662]
[2025-04-28 21:21:25,950 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:25,950 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,953 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:25,956 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:25,961 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:26,017 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 32 statements into 6 equivalence classes.
[2025-04-28 21:21:26,034 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:26,034 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 6 check-sat command(s)
[2025-04-28 21:21:26,035 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,036 INFO  L256         TraceCheckSpWp]: Trace formula consists of 64 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:26,038 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:26,279 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 6 proven. 30 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:26,279 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:27,281 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:27,281 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1715899662] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:27,281 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:27,281 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 14] total 23
[2025-04-28 21:21:27,282 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1708047393]
[2025-04-28 21:21:27,282 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,284 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:27,285 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,286 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:27,289 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=118, Invalid=388, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:27,289 INFO  L87              Difference]: Start difference. First operand 24 states and 25 transitions. Second operand  has 23 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 22 states have internal predecessors, (26), 12 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19)
[2025-04-28 21:21:27,504 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,504 INFO  L93              Difference]: Finished difference Result 26 states and 27 transitions.
[2025-04-28 21:21:27,504 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:27,505 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 22 states have internal predecessors, (26), 12 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19) Word has length 32
[2025-04-28 21:21:27,505 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,505 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:27,508 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:27,509 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 82 GetRequests, 53 SyntacticMatches, 3 SemanticMatches, 26 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 209 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=198, Invalid=558, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:27,510 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 35 mSDsluCounter, 86 mSDsCounter, 0 mSdLazyCounter, 54 mSolverCounterSat, 33 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 43 SdHoareTripleChecker+Valid, 102 SdHoareTripleChecker+Invalid, 87 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 33 IncrementalHoareTripleChecker+Valid, 54 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,510 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [43 Valid, 102 Invalid, 87 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [33 Valid, 54 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:27,511 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:27,521 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 26.
[2025-04-28 21:21:27,522 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:27,522 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 27 transitions.
[2025-04-28 21:21:27,522 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 27 transitions. Word has length 32
[2025-04-28 21:21:27,523 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,523 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 27 transitions.
[2025-04-28 21:21:27,523 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 22 states have internal predecessors, (26), 12 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (19), 9 states have call predecessors, (19), 12 states have call successors, (19)
[2025-04-28 21:21:27,523 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 27 transitions.
[2025-04-28 21:21:27,524 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:21:27,524 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,524 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:27,530 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:27,725 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:27,725 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,725 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,726 INFO  L85        PathProgramCache]: Analyzing trace with hash 1983750755, now seen corresponding path program 6 times
[2025-04-28 21:21:27,726 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,726 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2013558716]
[2025-04-28 21:21:27,726 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:27,726 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,731 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:27,752 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:27,753 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:27,753 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,235 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 1 proven. 53 refuted. 0 times theorem prover too weak. 24 trivial. 0 not checked.
[2025-04-28 21:21:28,235 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,235 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2013558716]
[2025-04-28 21:21:28,235 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2013558716] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,235 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1856130840]
[2025-04-28 21:21:28,236 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:28,236 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,239 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,241 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:28,245 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,309 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 36 statements into 7 equivalence classes.
[2025-04-28 21:21:28,327 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:28,328 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 7 check-sat command(s)
[2025-04-28 21:21:28,328 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,329 INFO  L256         TraceCheckSpWp]: Trace formula consists of 72 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,330 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,620 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 8 proven. 42 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:21:28,620 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:30,399 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:30,399 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1856130840] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:30,399 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:30,399 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 12, 16] total 27
[2025-04-28 21:21:30,400 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1873173074]
[2025-04-28 21:21:30,400 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,402 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:21:30,403 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,404 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:21:30,405 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=170, Invalid=532, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:30,405 INFO  L87              Difference]: Start difference. First operand 26 states and 27 transitions. Second operand  has 27 states, 12 states have (on average 2.5) internal successors, (30), 26 states have internal predecessors, (30), 16 states have call successors, (17), 1 states have call predecessors, (17), 11 states have return successors, (23), 9 states have call predecessors, (23), 16 states have call successors, (23)
[2025-04-28 21:21:30,636 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,636 INFO  L93              Difference]: Finished difference Result 28 states and 29 transitions.
[2025-04-28 21:21:30,637 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:30,638 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 12 states have (on average 2.5) internal successors, (30), 26 states have internal predecessors, (30), 16 states have call successors, (17), 1 states have call predecessors, (17), 11 states have return successors, (23), 9 states have call predecessors, (23), 16 states have call successors, (23) Word has length 36
[2025-04-28 21:21:30,638 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,638 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:30,639 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:30,639 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 93 GetRequests, 58 SyntacticMatches, 4 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 323 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=291, Invalid=765, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:30,640 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 23 mSDsluCounter, 99 mSDsCounter, 0 mSdLazyCounter, 56 mSolverCounterSat, 17 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 32 SdHoareTripleChecker+Valid, 114 SdHoareTripleChecker+Invalid, 73 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 17 IncrementalHoareTripleChecker+Valid, 56 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,640 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [32 Valid, 114 Invalid, 73 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [17 Valid, 56 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:30,641 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:30,645 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 28.
[2025-04-28 21:21:30,645 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:30,646 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 29 transitions.
[2025-04-28 21:21:30,646 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 29 transitions. Word has length 36
[2025-04-28 21:21:30,646 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,646 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 29 transitions.
[2025-04-28 21:21:30,647 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 12 states have (on average 2.5) internal successors, (30), 26 states have internal predecessors, (30), 16 states have call successors, (17), 1 states have call predecessors, (17), 11 states have return successors, (23), 9 states have call predecessors, (23), 16 states have call successors, (23)
[2025-04-28 21:21:30,647 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 29 transitions.
[2025-04-28 21:21:30,648 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:30,648 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,648 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:30,654 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:30,848 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:30,849 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,849 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,849 INFO  L85        PathProgramCache]: Analyzing trace with hash -2123555099, now seen corresponding path program 7 times
[2025-04-28 21:21:30,849 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,849 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [422442416]
[2025-04-28 21:21:30,849 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:30,849 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,854 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:30,860 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:30,861 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,861 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,214 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:31,215 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,215 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [422442416]
[2025-04-28 21:21:31,215 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [422442416] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,215 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1964301585]
[2025-04-28 21:21:31,215 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:21:31,216 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,218 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,221 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:31,224 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,301 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 40 statements into 1 equivalence classes.
[2025-04-28 21:21:31,323 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:31,323 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,323 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,325 INFO  L256         TraceCheckSpWp]: Trace formula consists of 80 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,326 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,597 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 10 proven. 56 refuted. 0 times theorem prover too weak. 39 trivial. 0 not checked.
[2025-04-28 21:21:31,598 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,875 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:33,875 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1964301585] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,875 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,875 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 13, 18] total 25
[2025-04-28 21:21:33,876 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [752694181]
[2025-04-28 21:21:33,876 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,876 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 25 states
[2025-04-28 21:21:33,876 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,877 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 25 interpolants.
[2025-04-28 21:21:33,878 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=166, Invalid=434, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:33,878 INFO  L87              Difference]: Start difference. First operand 28 states and 29 transitions. Second operand  has 25 states, 13 states have (on average 2.1538461538461537) internal successors, (28), 24 states have internal predecessors, (28), 13 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (25), 10 states have call predecessors, (25), 13 states have call successors, (25)
[2025-04-28 21:21:34,111 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,111 INFO  L93              Difference]: Finished difference Result 30 states and 31 transitions.
[2025-04-28 21:21:34,112 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:34,112 INFO  L79                 Accepts]: Start accepts. Automaton has  has 25 states, 13 states have (on average 2.1538461538461537) internal successors, (28), 24 states have internal predecessors, (28), 13 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (25), 10 states have call predecessors, (25), 13 states have call successors, (25) Word has length 40
[2025-04-28 21:21:34,113 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,113 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:34,113 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:34,114 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 104 GetRequests, 68 SyntacticMatches, 6 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 297 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=300, Invalid=692, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:34,115 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 39 mSDsluCounter, 110 mSDsCounter, 0 mSdLazyCounter, 57 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 49 SdHoareTripleChecker+Valid, 125 SdHoareTripleChecker+Invalid, 91 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 57 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,115 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [49 Valid, 125 Invalid, 91 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 57 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:34,116 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:34,120 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 30.
[2025-04-28 21:21:34,120 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:34,125 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 30 states to 30 states and 31 transitions.
[2025-04-28 21:21:34,126 INFO  L79                 Accepts]: Start accepts. Automaton has 30 states and 31 transitions. Word has length 40
[2025-04-28 21:21:34,126 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,126 INFO  L485      AbstractCegarLoop]: Abstraction has 30 states and 31 transitions.
[2025-04-28 21:21:34,126 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 25 states, 13 states have (on average 2.1538461538461537) internal successors, (28), 24 states have internal predecessors, (28), 13 states have call successors, (14), 1 states have call predecessors, (14), 12 states have return successors, (25), 10 states have call predecessors, (25), 13 states have call successors, (25)
[2025-04-28 21:21:34,127 INFO  L278                IsEmpty]: Start isEmpty. Operand 30 states and 31 transitions.
[2025-04-28 21:21:34,128 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:34,131 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,131 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:34,138 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:34,331 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:34,332 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,332 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,332 INFO  L85        PathProgramCache]: Analyzing trace with hash 797693031, now seen corresponding path program 8 times
[2025-04-28 21:21:34,333 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,333 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [258635825]
[2025-04-28 21:21:34,333 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:34,333 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,337 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 44 statements into 2 equivalence classes.
[2025-04-28 21:21:34,346 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:34,346 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:34,346 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,838 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:34,838 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,839 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [258635825]
[2025-04-28 21:21:34,839 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [258635825] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,839 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1472586446]
[2025-04-28 21:21:34,839 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:34,840 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,843 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,846 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:34,850 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,937 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 44 statements into 2 equivalence classes.
[2025-04-28 21:21:34,957 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:34,957 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:34,957 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,959 INFO  L256         TraceCheckSpWp]: Trace formula consists of 88 conjuncts, 25 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,962 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:35,279 INFO  L134       CoverageAnalysis]: Checked inductivity of 136 backedges. 12 proven. 72 refuted. 0 times theorem prover too weak. 52 trivial. 0 not checked.
[2025-04-28 21:21:35,279 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,839 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:38,839 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1472586446] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,840 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,840 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 14, 20] total 28
[2025-04-28 21:21:38,840 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1949461361]
[2025-04-28 21:21:38,840 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,840 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 28 states
[2025-04-28 21:21:38,841 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,842 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 28 interpolants.
[2025-04-28 21:21:38,842 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=200, Invalid=556, Unknown=0, NotChecked=0, Total=756
[2025-04-28 21:21:38,842 INFO  L87              Difference]: Start difference. First operand 30 states and 31 transitions. Second operand  has 28 states, 14 states have (on average 2.2142857142857144) internal successors, (31), 27 states have internal predecessors, (31), 15 states have call successors, (16), 1 states have call predecessors, (16), 13 states have return successors, (29), 11 states have call predecessors, (29), 15 states have call successors, (29)
[2025-04-28 21:21:39,098 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,099 INFO  L93              Difference]: Finished difference Result 32 states and 33 transitions.
[2025-04-28 21:21:39,099 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:39,100 INFO  L79                 Accepts]: Start accepts. Automaton has  has 28 states, 14 states have (on average 2.2142857142857144) internal successors, (31), 27 states have internal predecessors, (31), 15 states have call successors, (16), 1 states have call predecessors, (16), 13 states have return successors, (29), 11 states have call predecessors, (29), 15 states have call successors, (29) Word has length 44
[2025-04-28 21:21:39,100 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,101 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:39,101 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:39,102 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 115 GetRequests, 75 SyntacticMatches, 6 SemanticMatches, 34 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 385 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=369, Invalid=891, Unknown=0, NotChecked=0, Total=1260
[2025-04-28 21:21:39,102 INFO  L437           NwaCegarLoop]: 15 mSDtfsCounter, 10 mSDsluCounter, 134 mSDsCounter, 0 mSdLazyCounter, 71 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 21 SdHoareTripleChecker+Valid, 149 SdHoareTripleChecker+Invalid, 71 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 71 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,103 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [21 Valid, 149 Invalid, 71 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 71 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:39,103 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:39,107 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:21:39,107 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:39,108 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 33 transitions.
[2025-04-28 21:21:39,109 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 33 transitions. Word has length 44
[2025-04-28 21:21:39,109 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,109 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 33 transitions.
[2025-04-28 21:21:39,109 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 28 states, 14 states have (on average 2.2142857142857144) internal successors, (31), 27 states have internal predecessors, (31), 15 states have call successors, (16), 1 states have call predecessors, (16), 13 states have return successors, (29), 11 states have call predecessors, (29), 15 states have call successors, (29)
[2025-04-28 21:21:39,109 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 33 transitions.
[2025-04-28 21:21:39,110 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:21:39,110 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,111 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:39,119 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:39,311 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:39,312 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,312 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,312 INFO  L85        PathProgramCache]: Analyzing trace with hash 808108777, now seen corresponding path program 9 times
[2025-04-28 21:21:39,312 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,312 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [591109426]
[2025-04-28 21:21:39,313 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:39,313 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[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,340 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,341 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:39,341 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,046 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 4 proven. 116 refuted. 0 times theorem prover too weak. 51 trivial. 0 not checked.
[2025-04-28 21:21:40,046 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,046 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [591109426]
[2025-04-28 21:21:40,046 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [591109426] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,047 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1116245426]
[2025-04-28 21:21:40,047 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:40,047 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,050 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,052 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:40,057 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:40,173 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 48 statements into 10 equivalence classes.
[2025-04-28 21:21:40,204 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:40,204 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 10 check-sat command(s)
[2025-04-28 21:21:40,204 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,206 INFO  L256         TraceCheckSpWp]: Trace formula consists of 96 conjuncts, 30 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,208 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,526 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 110 refuted. 0 times theorem prover too weak. 61 trivial. 0 not checked.
[2025-04-28 21:21:40,526 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
