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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:19,226 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:19,306 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f60660ab-e6fd-444b-9662-27cfed9e21f6/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:19,312 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:19,313 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:19,335 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:19,336 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:19,336 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:19,337 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:19,337 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:19,337 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:19,337 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:19,337 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:19,338 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:19,338 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:19,338 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:19,338 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:19,338 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:19,338 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:19,338 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:19,338 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:19,339 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:19,339 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:19,339 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:19,339 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:19,340 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:19,340 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:19,687 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:19,700 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:19,703 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:19,705 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:19,707 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:19,708 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f60660ab-e6fd-444b-9662-27cfed9e21f6/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-109.smt2
[2025-04-28 21:21:19,710 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:19,714 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:19,905 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f60660ab-e6fd-444b-9662-27cfed9e21f6/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-109.smt2
[2025-04-28 21:21:19,908 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:19,911 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:19,912 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:19,912 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:19,912 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:19,919 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,944 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19 Unit
[2025-04-28 21:21:19,944 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:19,946 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:19,947 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:19,947 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:19,964 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,964 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,989 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,991 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,994 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,996 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,998 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:19,999 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:20,000 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:20,019 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:20,022 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:20,022 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:20,022 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:20,023 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (1/1) ...
[2025-04-28 21:21:20,026 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:20,047 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:20,060 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:20,065 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:20,076 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:20,076 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:20,076 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:20,076 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:20,077 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:20,077 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:20,077 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv1 given in one single declaration
[2025-04-28 21:21:20,077 INFO  L130     BoogieDeclarations]: Found specification of procedure inv1
[2025-04-28 21:21:20,077 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv1
[2025-04-28 21:21:20,077 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:20,077 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:20,077 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:20,121 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:20,123 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:20,228 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:20,229 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:20,245 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:20,246 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:20,246 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:20 BoogieIcfgContainer
[2025-04-28 21:21:20,246 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:20,252 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:20,252 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:20,259 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:20,259 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:19" (1/3) ...
[2025-04-28 21:21:20,260 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@15a59fd0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:20, skipping insertion in model container
[2025-04-28 21:21:20,260 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:19" (2/3) ...
[2025-04-28 21:21:20,260 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@15a59fd0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:20, skipping insertion in model container
[2025-04-28 21:21:20,261 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:20" (3/3) ...
[2025-04-28 21:21:20,262 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:20,285 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:20,288 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 18 locations, 26 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:20,335 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:20,348 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;@552fada8, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:20,349 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:20,358 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 18 states, 8 states have (on average 1.375) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 3 states have return successors, (5), 4 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:20,366 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:20,366 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,367 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,367 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,374 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,375 INFO  L85        PathProgramCache]: Analyzing trace with hash 171714104, now seen corresponding path program 1 times
[2025-04-28 21:21:20,384 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,385 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [126170136]
[2025-04-28 21:21:20,385 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,385 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,414 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:20,442 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:20,442 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,443 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,786 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:20,786 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,787 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [126170136]
[2025-04-28 21:21:20,788 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [126170136] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,788 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,791 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:20,794 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1144301508]
[2025-04-28 21:21:20,795 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,800 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:20,802 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,834 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:20,834 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:20,836 INFO  L87              Difference]: Start difference. First operand  has 18 states, 8 states have (on average 1.375) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 3 states have return successors, (5), 4 states have call predecessors, (5), 5 states have call successors, (5) Second operand  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:20,998 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,000 INFO  L93              Difference]: Finished difference Result 22 states and 27 transitions.
[2025-04-28 21:21:21,002 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:21,004 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3) Word has length 13
[2025-04-28 21:21:21,004 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,028 INFO  L225             Difference]: With dead ends: 22
[2025-04-28 21:21:21,029 INFO  L226             Difference]: Without dead ends: 22
[2025-04-28 21:21:21,031 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,034 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 3 mSDsluCounter, 50 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 66 SdHoareTripleChecker+Invalid, 28 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,035 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 66 Invalid, 28 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:21,082 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 22 states.
[2025-04-28 21:21:21,107 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 22 to 20.
[2025-04-28 21:21:21,108 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 20 states, 9 states have (on average 1.2222222222222223) internal successors, (11), 11 states have internal predecessors, (11), 5 states have call successors, (5), 3 states have call predecessors, (5), 5 states have return successors, (8), 5 states have call predecessors, (8), 5 states have call successors, (8)
[2025-04-28 21:21:21,119 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 24 transitions.
[2025-04-28 21:21:21,124 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 24 transitions. Word has length 13
[2025-04-28 21:21:21,124 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,125 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 24 transitions.
[2025-04-28 21:21:21,125 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 1.75) internal successors, (7), 5 states have internal predecessors, (7), 3 states have call successors, (3), 1 states have call predecessors, (3), 3 states have return successors, (3), 2 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:21,125 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 24 transitions.
[2025-04-28 21:21:21,127 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:21,127 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,127 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,130 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:21,130 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,133 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,133 INFO  L85        PathProgramCache]: Analyzing trace with hash 929256058, now seen corresponding path program 1 times
[2025-04-28 21:21:21,133 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,133 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [96225519]
[2025-04-28 21:21:21,140 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,141 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,160 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:21,181 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:21,181 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,181 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,459 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:21,460 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,460 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [96225519]
[2025-04-28 21:21:21,461 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [96225519] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:21,461 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [355699922]
[2025-04-28 21:21:21,461 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,461 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:21,465 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:21,470 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:21,472 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:21,513 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:21,538 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:21,539 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,539 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,541 INFO  L256         TraceCheckSpWp]: Trace formula consists of 62 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:21,549 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:21,789 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:21,790 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:22,835 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:22,839 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [355699922] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:22,840 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:22,840 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 15
[2025-04-28 21:21:22,841 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [295625386]
[2025-04-28 21:21:22,841 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:22,841 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:22,842 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:22,842 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:22,843 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=42, Invalid=168, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:22,846 INFO  L87              Difference]: Start difference. First operand 20 states and 24 transitions. Second operand  has 15 states, 8 states have (on average 2.125) internal successors, (17), 14 states have internal predecessors, (17), 8 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:23,099 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,099 INFO  L93              Difference]: Finished difference Result 26 states and 32 transitions.
[2025-04-28 21:21:23,100 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:23,100 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 8 states have (on average 2.125) internal successors, (17), 14 states have internal predecessors, (17), 8 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10) Word has length 17
[2025-04-28 21:21:23,100 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,101 INFO  L225             Difference]: With dead ends: 26
[2025-04-28 21:21:23,101 INFO  L226             Difference]: Without dead ends: 26
[2025-04-28 21:21:23,102 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 44 GetRequests, 28 SyntacticMatches, 0 SemanticMatches, 16 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 38 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=65, Invalid=241, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:23,102 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 5 mSDsluCounter, 140 mSDsCounter, 0 mSdLazyCounter, 128 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 157 SdHoareTripleChecker+Invalid, 129 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 128 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,103 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 157 Invalid, 129 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 128 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:23,104 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 26 states.
[2025-04-28 21:21:23,107 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 26 to 22.
[2025-04-28 21:21:23,108 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 10 states have (on average 1.2) internal successors, (12), 12 states have internal predecessors, (12), 5 states have call successors, (5), 3 states have call predecessors, (5), 6 states have return successors, (9), 6 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:23,110 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 26 transitions.
[2025-04-28 21:21:23,110 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 26 transitions. Word has length 17
[2025-04-28 21:21:23,110 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,111 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 26 transitions.
[2025-04-28 21:21:23,111 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 8 states have (on average 2.125) internal successors, (17), 14 states have internal predecessors, (17), 8 states have call successors, (8), 1 states have call predecessors, (8), 7 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:23,111 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 26 transitions.
[2025-04-28 21:21:23,112 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:23,112 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,113 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:23,120 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:23,317 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:23,317 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,317 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,318 INFO  L85        PathProgramCache]: Analyzing trace with hash -1864212420, now seen corresponding path program 1 times
[2025-04-28 21:21:23,318 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,318 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [563485643]
[2025-04-28 21:21:23,318 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,318 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,323 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:23,330 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:23,331 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,331 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,531 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:23,531 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,532 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [563485643]
[2025-04-28 21:21:23,532 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [563485643] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:23,532 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:23,532 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:23,532 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [255637508]
[2025-04-28 21:21:23,532 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:23,532 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:23,532 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:23,533 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:23,533 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:23,533 INFO  L87              Difference]: Start difference. First operand 22 states and 26 transitions. Second operand  has 8 states, 5 states have (on average 1.8) internal successors, (9), 7 states have internal predecessors, (9), 4 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:23,622 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,622 INFO  L93              Difference]: Finished difference Result 24 states and 28 transitions.
[2025-04-28 21:21:23,623 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:23,623 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 1.8) internal successors, (9), 7 states have internal predecessors, (9), 4 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4) Word has length 17
[2025-04-28 21:21:23,624 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,624 INFO  L225             Difference]: With dead ends: 24
[2025-04-28 21:21:23,624 INFO  L226             Difference]: Without dead ends: 24
[2025-04-28 21:21:23,625 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 3 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:23,626 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 3 mSDsluCounter, 64 mSDsCounter, 0 mSdLazyCounter, 40 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 82 SdHoareTripleChecker+Invalid, 40 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 40 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,626 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 82 Invalid, 40 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 40 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:23,627 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 24 states.
[2025-04-28 21:21:23,630 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 24 to 22.
[2025-04-28 21:21:23,630 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 22 states, 10 states have (on average 1.2) internal successors, (12), 12 states have internal predecessors, (12), 5 states have call successors, (5), 3 states have call predecessors, (5), 6 states have return successors, (9), 6 states have call predecessors, (9), 5 states have call successors, (9)
[2025-04-28 21:21:23,631 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 22 states to 22 states and 26 transitions.
[2025-04-28 21:21:23,631 INFO  L79                 Accepts]: Start accepts. Automaton has 22 states and 26 transitions. Word has length 17
[2025-04-28 21:21:23,631 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,631 INFO  L485      AbstractCegarLoop]: Abstraction has 22 states and 26 transitions.
[2025-04-28 21:21:23,632 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 1.8) internal successors, (9), 7 states have internal predecessors, (9), 4 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:23,634 INFO  L278                IsEmpty]: Start isEmpty. Operand 22 states and 26 transitions.
[2025-04-28 21:21:23,635 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:23,636 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,637 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:23,637 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:23,637 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,637 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,638 INFO  L85        PathProgramCache]: Analyzing trace with hash 1746654140, now seen corresponding path program 2 times
[2025-04-28 21:21:23,638 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,638 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1247169476]
[2025-04-28 21:21:23,639 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:23,639 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,646 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:21:23,661 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:23,661 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:23,661 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,964 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:23,964 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,964 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1247169476]
[2025-04-28 21:21:23,964 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1247169476] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:23,964 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [428801112]
[2025-04-28 21:21:23,964 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:23,965 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:23,967 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:23,971 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:23,974 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:24,017 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:21:24,036 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:24,036 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:24,037 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,038 INFO  L256         TraceCheckSpWp]: Trace formula consists of 81 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:24,040 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:24,200 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:24,200 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:25,607 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:25,608 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [428801112] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:25,608 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:25,608 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 10] total 18
[2025-04-28 21:21:25,608 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [554995344]
[2025-04-28 21:21:25,608 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,608 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 18 states
[2025-04-28 21:21:25,609 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,609 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 18 interpolants.
[2025-04-28 21:21:25,610 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=67, Invalid=239, Unknown=0, NotChecked=0, Total=306
[2025-04-28 21:21:25,610 INFO  L87              Difference]: Start difference. First operand 22 states and 26 transitions. Second operand  has 18 states, 10 states have (on average 2.0) internal successors, (20), 17 states have internal predecessors, (20), 9 states have call successors, (9), 1 states have call predecessors, (9), 9 states have return successors, (13), 7 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:25,807 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,807 INFO  L93              Difference]: Finished difference Result 28 states and 33 transitions.
[2025-04-28 21:21:25,808 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:25,808 INFO  L79                 Accepts]: Start accepts. Automaton has  has 18 states, 10 states have (on average 2.0) internal successors, (20), 17 states have internal predecessors, (20), 9 states have call successors, (9), 1 states have call predecessors, (9), 9 states have return successors, (13), 7 states have call predecessors, (13), 9 states have call successors, (13) Word has length 21
[2025-04-28 21:21:25,808 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,809 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:25,809 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:25,809 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 55 GetRequests, 35 SyntacticMatches, 0 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 72 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=110, Invalid=352, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:25,810 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 6 mSDsluCounter, 129 mSDsCounter, 0 mSdLazyCounter, 105 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 146 SdHoareTripleChecker+Invalid, 108 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 105 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:25,811 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 146 Invalid, 108 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 105 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:25,811 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:25,815 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 24.
[2025-04-28 21:21:25,815 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 13 states have internal predecessors, (13), 5 states have call successors, (5), 3 states have call predecessors, (5), 7 states have return successors, (10), 7 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:21:25,816 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 28 transitions.
[2025-04-28 21:21:25,816 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 28 transitions. Word has length 21
[2025-04-28 21:21:25,816 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,816 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 28 transitions.
[2025-04-28 21:21:25,816 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 18 states, 10 states have (on average 2.0) internal successors, (20), 17 states have internal predecessors, (20), 9 states have call successors, (9), 1 states have call predecessors, (9), 9 states have return successors, (13), 7 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:21:25,817 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 28 transitions.
[2025-04-28 21:21:25,817 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:25,817 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,817 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:25,822 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:26,022 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:26,022 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,023 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,023 INFO  L85        PathProgramCache]: Analyzing trace with hash 1578006782, now seen corresponding path program 1 times
[2025-04-28 21:21:26,023 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,023 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1279277337]
[2025-04-28 21:21:26,023 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,023 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,028 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:26,032 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:26,033 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,033 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,203 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:26,205 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,205 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1279277337]
[2025-04-28 21:21:26,205 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1279277337] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:26,205 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [774646376]
[2025-04-28 21:21:26,205 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,205 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:26,208 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:26,212 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:26,215 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:26,263 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:26,275 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:26,275 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,275 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,276 INFO  L256         TraceCheckSpWp]: Trace formula consists of 76 conjuncts, 14 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:26,278 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:26,421 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:26,421 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:27,579 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:27,580 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [774646376] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:27,580 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:27,580 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 19
[2025-04-28 21:21:27,580 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1607578487]
[2025-04-28 21:21:27,580 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:27,580 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:27,580 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:27,581 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:27,581 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=56, Invalid=286, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:27,581 INFO  L87              Difference]: Start difference. First operand 24 states and 28 transitions. Second operand  has 19 states, 10 states have (on average 2.1) internal successors, (21), 18 states have internal predecessors, (21), 10 states have call successors, (10), 1 states have call predecessors, (10), 9 states have return successors, (13), 7 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:27,759 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,759 INFO  L93              Difference]: Finished difference Result 30 states and 35 transitions.
[2025-04-28 21:21:27,760 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:27,760 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 10 states have (on average 2.1) internal successors, (21), 18 states have internal predecessors, (21), 10 states have call successors, (10), 1 states have call predecessors, (10), 9 states have return successors, (13), 7 states have call predecessors, (13), 10 states have call successors, (13) Word has length 21
[2025-04-28 21:21:27,760 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,761 INFO  L225             Difference]: With dead ends: 30
[2025-04-28 21:21:27,761 INFO  L226             Difference]: Without dead ends: 30
[2025-04-28 21:21:27,762 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 34 SyntacticMatches, 0 SemanticMatches, 22 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 83 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=94, Invalid=458, Unknown=0, NotChecked=0, Total=552
[2025-04-28 21:21:27,762 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 11 mSDsluCounter, 110 mSDsCounter, 0 mSdLazyCounter, 94 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 128 SdHoareTripleChecker+Invalid, 100 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 94 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,763 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 128 Invalid, 100 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 94 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:27,763 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 30 states.
[2025-04-28 21:21:27,766 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 30 to 24.
[2025-04-28 21:21:27,767 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 11 states have (on average 1.1818181818181819) internal successors, (13), 13 states have internal predecessors, (13), 5 states have call successors, (5), 3 states have call predecessors, (5), 7 states have return successors, (10), 7 states have call predecessors, (10), 5 states have call successors, (10)
[2025-04-28 21:21:27,767 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 28 transitions.
[2025-04-28 21:21:27,767 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 28 transitions. Word has length 21
[2025-04-28 21:21:27,768 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,768 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 28 transitions.
[2025-04-28 21:21:27,768 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 10 states have (on average 2.1) internal successors, (21), 18 states have internal predecessors, (21), 10 states have call successors, (10), 1 states have call predecessors, (10), 9 states have return successors, (13), 7 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:27,768 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 28 transitions.
[2025-04-28 21:21:27,768 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:27,769 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,769 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:27,773 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:27,973 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,973 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,973 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,973 INFO  L85        PathProgramCache]: Analyzing trace with hash -713446914, now seen corresponding path program 3 times
[2025-04-28 21:21:27,974 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,974 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1042363899]
[2025-04-28 21:21:27,974 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:27,974 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,979 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 25 statements into 4 equivalence classes.
[2025-04-28 21:21:27,990 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:27,990 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:27,990 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,268 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 14 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:28,268 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:28,269 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1042363899]
[2025-04-28 21:21:28,269 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1042363899] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:28,269 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2097513164]
[2025-04-28 21:21:28,269 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:28,269 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:28,272 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:28,274 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:28,278 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:28,332 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 25 statements into 4 equivalence classes.
[2025-04-28 21:21:28,352 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:28,352 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:28,352 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,353 INFO  L256         TraceCheckSpWp]: Trace formula consists of 100 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,355 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,500 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:28,500 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:30,248 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:30,248 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2097513164] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:30,249 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:30,249 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 10, 12] total 21
[2025-04-28 21:21:30,249 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [997778295]
[2025-04-28 21:21:30,249 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,249 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:30,249 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,250 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:30,250 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=91, Invalid=329, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:30,250 INFO  L87              Difference]: Start difference. First operand 24 states and 28 transitions. Second operand  has 21 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 20 states have internal predecessors, (23), 10 states have call successors, (10), 1 states have call predecessors, (10), 11 states have return successors, (16), 9 states have call predecessors, (16), 10 states have call successors, (16)
[2025-04-28 21:21:30,440 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,440 INFO  L93              Difference]: Finished difference Result 32 states and 37 transitions.
[2025-04-28 21:21:30,440 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:30,441 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 20 states have internal predecessors, (23), 10 states have call successors, (10), 1 states have call predecessors, (10), 11 states have return successors, (16), 9 states have call predecessors, (16), 10 states have call successors, (16) Word has length 25
[2025-04-28 21:21:30,441 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,442 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:30,442 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:30,442 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 42 SyntacticMatches, 0 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 119 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=157, Invalid=493, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:30,443 INFO  L437           NwaCegarLoop]: 17 mSDtfsCounter, 9 mSDsluCounter, 139 mSDsCounter, 0 mSdLazyCounter, 105 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 156 SdHoareTripleChecker+Invalid, 114 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 105 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,443 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 156 Invalid, 114 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 105 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:30,444 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:30,448 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 26.
[2025-04-28 21:21:30,448 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 5 states have call successors, (5), 3 states have call predecessors, (5), 8 states have return successors, (11), 8 states have call predecessors, (11), 5 states have call successors, (11)
[2025-04-28 21:21:30,449 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 30 transitions.
[2025-04-28 21:21:30,449 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 30 transitions. Word has length 25
[2025-04-28 21:21:30,449 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,449 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 30 transitions.
[2025-04-28 21:21:30,449 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 20 states have internal predecessors, (23), 10 states have call successors, (10), 1 states have call predecessors, (10), 11 states have return successors, (16), 9 states have call predecessors, (16), 10 states have call successors, (16)
[2025-04-28 21:21:30,449 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 30 transitions.
[2025-04-28 21:21:30,450 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:30,450 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,450 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:30,454 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:30,651 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,651 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,652 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,652 INFO  L85        PathProgramCache]: Analyzing trace with hash 425199296, now seen corresponding path program 2 times
[2025-04-28 21:21:30,652 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,652 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1483368560]
[2025-04-28 21:21:30,652 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:30,652 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,656 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:30,662 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:30,662 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:30,662 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,912 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 6 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:30,912 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,912 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1483368560]
[2025-04-28 21:21:30,912 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1483368560] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:30,912 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1788682617]
[2025-04-28 21:21:30,912 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:30,912 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,915 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:30,917 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:30,921 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:30,989 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:31,004 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:31,005 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:31,005 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,006 INFO  L256         TraceCheckSpWp]: Trace formula consists of 95 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,007 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,152 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 6 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:31,152 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:32,813 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:32,813 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1788682617] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:32,813 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:32,813 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 11, 12] total 21
[2025-04-28 21:21:32,813 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1446615856]
[2025-04-28 21:21:32,813 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,814 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:21:32,814 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,815 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:21:32,815 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=70, Invalid=350, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:32,816 INFO  L87              Difference]: Start difference. First operand 26 states and 30 transitions. Second operand  has 21 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 20 states have internal predecessors, (23), 10 states have call successors, (10), 1 states have call predecessors, (10), 11 states have return successors, (16), 9 states have call predecessors, (16), 10 states have call successors, (16)
[2025-04-28 21:21:33,049 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,050 INFO  L93              Difference]: Finished difference Result 34 states and 39 transitions.
[2025-04-28 21:21:33,050 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:33,050 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 20 states have internal predecessors, (23), 10 states have call successors, (10), 1 states have call predecessors, (10), 11 states have return successors, (16), 9 states have call predecessors, (16), 10 states have call successors, (16) Word has length 25
[2025-04-28 21:21:33,051 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,051 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:33,051 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:33,052 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 67 GetRequests, 42 SyntacticMatches, 0 SemanticMatches, 25 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 122 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=125, Invalid=577, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:21:33,053 INFO  L437           NwaCegarLoop]: 18 mSDtfsCounter, 14 mSDsluCounter, 135 mSDsCounter, 0 mSdLazyCounter, 116 mSolverCounterSat, 10 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 153 SdHoareTripleChecker+Invalid, 126 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 10 IncrementalHoareTripleChecker+Valid, 116 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,053 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 153 Invalid, 126 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [10 Valid, 116 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:33,054 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:33,058 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 26.
[2025-04-28 21:21:33,058 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 26 states, 12 states have (on average 1.1666666666666667) internal successors, (14), 14 states have internal predecessors, (14), 5 states have call successors, (5), 3 states have call predecessors, (5), 8 states have return successors, (11), 8 states have call predecessors, (11), 5 states have call successors, (11)
[2025-04-28 21:21:33,059 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 26 states to 26 states and 30 transitions.
[2025-04-28 21:21:33,059 INFO  L79                 Accepts]: Start accepts. Automaton has 26 states and 30 transitions. Word has length 25
[2025-04-28 21:21:33,059 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,059 INFO  L485      AbstractCegarLoop]: Abstraction has 26 states and 30 transitions.
[2025-04-28 21:21:33,059 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 12 states have (on average 1.9166666666666667) internal successors, (23), 20 states have internal predecessors, (23), 10 states have call successors, (10), 1 states have call predecessors, (10), 11 states have return successors, (16), 9 states have call predecessors, (16), 10 states have call successors, (16)
[2025-04-28 21:21:33,059 INFO  L278                IsEmpty]: Start isEmpty. Operand 26 states and 30 transitions.
[2025-04-28 21:21:33,060 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:33,060 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,060 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:33,066 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:33,261 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,261 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,261 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,262 INFO  L85        PathProgramCache]: Analyzing trace with hash 921752896, now seen corresponding path program 4 times
[2025-04-28 21:21:33,262 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,262 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [397915232]
[2025-04-28 21:21:33,262 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:33,262 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,266 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:33,292 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 28 of 29 statements.
[2025-04-28 21:21:33,296 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:33,296 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,066 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:34,066 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,067 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [397915232]
[2025-04-28 21:21:34,067 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [397915232] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,067 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1305657942]
[2025-04-28 21:21:34,067 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:34,067 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,069 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,072 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:34,075 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,152 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:34,170 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 28 of 29 statements.
[2025-04-28 21:21:34,170 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:34,170 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,172 WARN  L254         TraceCheckSpWp]: Trace formula consists of 117 conjuncts, 64 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,176 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,648 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:34,649 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:36,369 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:36,369 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1305657942] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:36,370 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:36,370 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 11, 13] total 26
[2025-04-28 21:21:36,370 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [951610705]
[2025-04-28 21:21:36,370 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,370 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:36,370 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,371 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:36,371 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=75, Invalid=575, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:36,372 INFO  L87              Difference]: Start difference. First operand 26 states and 30 transitions. Second operand  has 26 states, 14 states have (on average 2.0714285714285716) internal successors, (29), 26 states have internal predecessors, (29), 13 states have call successors, (14), 1 states have call predecessors, (14), 13 states have return successors, (18), 11 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:21:36,767 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,767 INFO  L93              Difference]: Finished difference Result 34 states and 38 transitions.
[2025-04-28 21:21:36,768 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:36,768 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 14 states have (on average 2.0714285714285716) internal successors, (29), 26 states have internal predecessors, (29), 13 states have call successors, (14), 1 states have call predecessors, (14), 13 states have return successors, (18), 11 states have call predecessors, (18), 13 states have call successors, (18) Word has length 29
[2025-04-28 21:21:36,768 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,769 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:36,769 INFO  L226             Difference]: Without dead ends: 0
[2025-04-28 21:21:36,769 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 77 GetRequests, 46 SyntacticMatches, 0 SemanticMatches, 31 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 149 ImplicationChecksByTransitivity, 0.8s TimeCoverageRelationStatistics Valid=192, Invalid=864, Unknown=0, NotChecked=0, Total=1056
[2025-04-28 21:21:36,770 INFO  L437           NwaCegarLoop]: 16 mSDtfsCounter, 22 mSDsluCounter, 172 mSDsCounter, 0 mSdLazyCounter, 124 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 188 SdHoareTripleChecker+Invalid, 158 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 124 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,771 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 188 Invalid, 158 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 124 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,772 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 0 states.
[2025-04-28 21:21:36,772 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 0 to 0.
[2025-04-28 21:21:36,772 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 0 states, 0 states have (on average 0.0) internal successors, (0), 0 states have internal predecessors, (0), 0 states have call successors, (0), 0 states have call predecessors, (0), 0 states have return successors, (0), 0 states have call predecessors, (0), 0 states have call successors, (0)
[2025-04-28 21:21:36,772 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 0 states to 0 states and 0 transitions.
[2025-04-28 21:21:36,773 INFO  L79                 Accepts]: Start accepts. Automaton has 0 states and 0 transitions. Word has length 29
[2025-04-28 21:21:36,773 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,773 INFO  L485      AbstractCegarLoop]: Abstraction has 0 states and 0 transitions.
[2025-04-28 21:21:36,773 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 14 states have (on average 2.0714285714285716) internal successors, (29), 26 states have internal predecessors, (29), 13 states have call successors, (14), 1 states have call predecessors, (14), 13 states have return successors, (18), 11 states have call predecessors, (18), 13 states have call successors, (18)
[2025-04-28 21:21:36,773 INFO  L278                IsEmpty]: Start isEmpty. Operand 0 states and 0 transitions.
[2025-04-28 21:21:36,773 INFO  L284                IsEmpty]: Finished isEmpty. No accepting run.
[2025-04-28 21:21:36,776 INFO  L790   garLoopResultBuilder]: Registering result SAFE for location Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY (0 of 1 remaining)
[2025-04-28 21:21:36,780 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:36,977 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,980 INFO  L422         BasicCegarLoop]: Path program histogram: [4, 2, 1, 1]
[2025-04-28 21:21:36,982 INFO  L171   ceAbstractionStarter]: Computing trace abstraction results
[2025-04-28 21:21:36,987 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction CFG 28.04 09:21:36 BoogieIcfgContainer
[2025-04-28 21:21:36,987 INFO  L131        PluginConnector]: ------------------------ END TraceAbstraction----------------------------
[2025-04-28 21:21:36,988 INFO  L158              Benchmark]: Toolchain (without parser) took 17076.71ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 165.3MB in the beginning and 110.5MB in the end (delta: 54.8MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:36,988 INFO  L158              Benchmark]: SmtParser took 0.42ms. Allocated memory is still 234.9MB. Free memory is still 171.9MB. There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:36,988 INFO  L158              Benchmark]: ChcToBoogie took 33.36ms. Allocated memory is still 234.9MB. Free memory was 165.3MB in the beginning and 164.4MB in the end (delta: 899.3kB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:36,988 INFO  L158              Benchmark]: Boogie Preprocessor took 74.95ms. Allocated memory is still 234.9MB. Free memory was 164.4MB in the beginning and 162.0MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:36,989 INFO  L158              Benchmark]: RCFGBuilder took 224.15ms. Allocated memory is still 234.9MB. Free memory was 162.0MB in the beginning and 152.9MB in the end (delta: 9.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
[2025-04-28 21:21:36,989 INFO  L158              Benchmark]: TraceAbstraction took 16734.61ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 152.5MB in the beginning and 110.5MB in the end (delta: 42.0MB). There was no memory consumed. Max. memory is 33.6GB.
[2025-04-28 21:21:36,990 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.42ms. Allocated memory is still 234.9MB. Free memory is still 171.9MB. There was no memory consumed. Max. memory is 33.6GB.
 * ChcToBoogie took 33.36ms. Allocated memory is still 234.9MB. Free memory was 165.3MB in the beginning and 164.4MB in the end (delta: 899.3kB). There was no memory consumed. Max. memory is 33.6GB.
 * Boogie Preprocessor took 74.95ms. Allocated memory is still 234.9MB. Free memory was 164.4MB in the beginning and 162.0MB in the end (delta: 2.4MB). There was no memory consumed. Max. memory is 33.6GB.
 * RCFGBuilder took 224.15ms. Allocated memory is still 234.9MB. Free memory was 162.0MB in the beginning and 152.9MB in the end (delta: 9.1MB). Peak memory consumption was 16.8MB. Max. memory is 33.6GB.
 * TraceAbstraction took 16734.61ms. Allocated memory was 234.9MB in the beginning and 167.8MB in the end (delta: -67.1MB). Free memory was 152.5MB in the beginning and 110.5MB in the end (delta: 42.0MB). There was no memory consumed. Max. memory is 33.6GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - StatisticsResult: ErrorAutomatonStatistics
    NumberErrorTraces: 0, NumberStatementsAllTraces: 0, NumberRelevantStatements: 0, 0.0s ErrorAutomatonConstructionTimeTotal, 0.0s FaulLocalizationTime, NumberStatementsFirstTrace: -1, TraceLengthAvg: 0, 0.0s ErrorAutomatonConstructionTimeAvg, 0.0s ErrorAutomatonDifferenceTimeAvg, 0.0s ErrorAutomatonDifferenceTimeTotal, NumberOfNoEnhancement: 0, NumberOfFiniteEnhancement: 0, NumberOfInfiniteEnhancement: 0
  - PositiveResult [Unknown line] : the set of constraint Horn clauses is satisfiable
    For all program executions holds that the set of constraint Horn clauses is satisfiable at this location
  - StatisticsResult: Ultimate Automizer benchmark data
    CFG has 4 procedures, 18 locations, 26 edges, 1 error locations. Started 1 CEGAR loops. OverallTime: 16.7s, OverallIterations: 8, TraceHistogramMax: 5, PathProgramHistogramMax: 4, EmptinessCheckTime: 0.0s, AutomataDifference: 1.8s, DeadEndRemovalTime: 0.0s, HoareAnnotationTime: 0.0s, InitialAbstractionConstructionTime: 0.0s, HoareTripleCheckerStatistics: 0 mSolverCounterUnknown, 114 SdHoareTripleChecker+Valid, 0.9s IncrementalHoareTripleChecker+Time, 0 mSdLazyCounter, 73 mSDsluCounter, 1076 SdHoareTripleChecker+Invalid, 0.8s Time, 0 mProtectedAction, 0 SdHoareTripleChecker+Unchecked, 0 IncrementalHoareTripleChecker+Unchecked, 939 mSDsCounter, 63 IncrementalHoareTripleChecker+Valid, 0 mProtectedPredicate, 740 IncrementalHoareTripleChecker+Invalid, 803 SdHoareTripleChecker+Unknown, 0 mSolverCounterNotChecked, 63 mSolverCounterUnsat, 137 mSDtfsCounter, 740 mSolverCounterSat, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Unknown, PredicateUnifierStatistics: 0 DeclaredPredicates, 382 GetRequests, 231 SyntacticMatches, 0 SemanticMatches, 151 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 586 ImplicationChecksByTransitivity, 2.5s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=26occurred in iteration=6, InterpolantAutomatonStates: 81, traceCheckStatistics: No data available, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s DumpTime, AutomataMinimizationStatistics: 0.1s AutomataMinimizationTime, 8 MinimizatonAttempts, 32 StatesRemovedByMinimization, 7 NontrivialMinimizations, HoareAnnotationStatistics: No data available, RefinementEngineStatistics: TRACE_CHECK: 0.0s SsaConstructionTime, 0.3s SatisfiabilityAnalysisTime, 12.7s InterpolantComputationTime, 306 NumberOfCodeBlocks, 304 NumberOfCodeBlocksAsserted, 24 NumberOfCheckSat, 424 ConstructedInterpolants, 0 QuantifiedInterpolants, 2329 SizeOfPredicates, 70 NumberOfNonLiveVariables, 531 ConjunctsInSsa, 137 ConjunctsInUnsatCore, 20 InterpolantComputations, 2 PerfectInterpolantSequences, 103/270 InterpolantCoveringCapability, INVARIANT_SYNTHESIS: No data available, INTERPOLANT_CONSOLIDATION: No data available, ABSTRACT_INTERPRETATION: No data available, PDR: No data available, ACCELERATED_INTERPOLATION: No data available, SIFA: No data available, ReuseStatistics: No data available, ConComCheckerStatistics: No data available
  - AllSpecificationsHoldResult: All specifications hold
    1 specifications checked. All of them hold
RESULT: Ultimate proved your program to be correct!
[2025-04-28 21:21:37,008 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Ended with exit code 0
Received shutdown request...
sat
