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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:41,768 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:41,864 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_51ce970a-1781-40df-94b3-70868a035983/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:41,874 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:41,874 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:41,904 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:41,906 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:41,906 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:41,907 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:41,908 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:41,909 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:41,909 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:41,909 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:41,910 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:41,910 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:41,910 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:41,910 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:41,910 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:41,911 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,911 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:41,911 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:41,911 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:41,912 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:41,912 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:41,912 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:41,912 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:41,913 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:42,263 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:42,275 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:42,278 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:42,279 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:42,281 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:42,283 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_51ce970a-1781-40df-94b3-70868a035983/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-030.smt2
[2025-04-28 21:21:42,285 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:42,289 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:42,584 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_51ce970a-1781-40df-94b3-70868a035983/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-030.smt2
[2025-04-28 21:21:42,587 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:42,589 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:42,590 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:42,590 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:42,590 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:42,593 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,624 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42 Unit
[2025-04-28 21:21:42,625 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:42,627 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:42,627 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:42,627 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:42,648 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,648 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,676 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,676 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,682 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,684 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,686 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,687 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,688 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,711 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:42,712 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:42,712 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:42,713 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:42,714 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (1/1) ...
[2025-04-28 21:21:42,717 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:42,737 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,752 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:42,756 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:42,768 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:42,768 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:42,768 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:42,768 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure state given in one single declaration
[2025-04-28 21:21:42,768 INFO  L130     BoogieDeclarations]: Found specification of procedure state
[2025-04-28 21:21:42,768 INFO  L138     BoogieDeclarations]: Found implementation of procedure state
[2025-04-28 21:21:42,768 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:42,769 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:42,769 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:42,824 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:42,827 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:42,987 INFO  L?                        ?]: Removed 1 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:42,987 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:43,005 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:43,006 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:43,009 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:43 BoogieIcfgContainer
[2025-04-28 21:21:43,009 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:43,012 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:43,014 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:43,018 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:43,019 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:42" (1/3) ...
[2025-04-28 21:21:43,020 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@469c2845 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:43, skipping insertion in model container
[2025-04-28 21:21:43,020 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:42" (2/3) ...
[2025-04-28 21:21:43,020 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@469c2845 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:43, skipping insertion in model container
[2025-04-28 21:21:43,020 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:43" (3/3) ...
[2025-04-28 21:21:43,022 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:43,038 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:43,040 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 13 locations, 17 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:43,082 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:43,095 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;@4678f3c4, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:43,095 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:43,100 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 13 states, 6 states have (on average 1.3333333333333333) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 2 states have return successors, (3), 3 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:43,110 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:43,111 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,111 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,112 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,118 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,119 INFO  L85        PathProgramCache]: Analyzing trace with hash -597537630, now seen corresponding path program 1 times
[2025-04-28 21:21:43,128 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,130 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [746777896]
[2025-04-28 21:21:43,130 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,131 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,156 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:43,164 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:43,165 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,165 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,278 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:43,278 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,278 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [746777896]
[2025-04-28 21:21:43,279 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [746777896] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,279 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,282 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:43,284 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1784019552]
[2025-04-28 21:21:43,284 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,291 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:43,293 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,325 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:43,326 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:43,328 INFO  L87              Difference]: Start difference. First operand  has 13 states, 6 states have (on average 1.3333333333333333) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 2 states have return successors, (3), 3 states have call predecessors, (3), 3 states have call successors, (3) Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:43,384 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,385 INFO  L93              Difference]: Finished difference Result 13 states and 14 transitions.
[2025-04-28 21:21:43,386 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:43,388 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:43,388 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,394 INFO  L225             Difference]: With dead ends: 13
[2025-04-28 21:21:43,394 INFO  L226             Difference]: Without dead ends: 13
[2025-04-28 21:21:43,396 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:43,399 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 1 mSDsluCounter, 15 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 26 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,400 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 26 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:43,413 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 13 states.
[2025-04-28 21:21:43,433 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 13 to 13.
[2025-04-28 21:21:43,434 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 13 states, 6 states have (on average 1.1666666666666667) internal successors, (7), 7 states have internal predecessors, (7), 3 states have call successors, (3), 2 states have call predecessors, (3), 3 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:43,440 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 13 states to 13 states and 14 transitions.
[2025-04-28 21:21:43,442 INFO  L79                 Accepts]: Start accepts. Automaton has 13 states and 14 transitions. Word has length 9
[2025-04-28 21:21:43,442 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,443 INFO  L485      AbstractCegarLoop]: Abstraction has 13 states and 14 transitions.
[2025-04-28 21:21:43,443 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:43,443 INFO  L278                IsEmpty]: Start isEmpty. Operand 13 states and 14 transitions.
[2025-04-28 21:21:43,444 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:43,444 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,445 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,445 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:43,445 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,446 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,446 INFO  L85        PathProgramCache]: Analyzing trace with hash 1530833734, now seen corresponding path program 1 times
[2025-04-28 21:21:43,446 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,446 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1856056966]
[2025-04-28 21:21:43,446 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,447 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,458 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:43,503 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:43,504 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,504 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,080 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:44,081 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,081 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1856056966]
[2025-04-28 21:21:44,081 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1856056966] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:44,081 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2040078125]
[2025-04-28 21:21:44,081 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,082 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,086 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,090 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:44,093 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,142 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:44,171 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:44,171 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,171 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,174 INFO  L256         TraceCheckSpWp]: Trace formula consists of 82 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,178 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,395 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:44,395 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,426 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:45,427 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2040078125] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,427 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,427 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 9
[2025-04-28 21:21:45,427 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [803366050]
[2025-04-28 21:21:45,429 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,429 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:45,430 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,431 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:45,431 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=19, Invalid=53, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:45,432 INFO  L87              Difference]: Start difference. First operand 13 states and 14 transitions. Second operand  has 9 states, 5 states have (on average 2.0) internal successors, (10), 8 states have internal predecessors, (10), 5 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:45,562 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,562 INFO  L93              Difference]: Finished difference Result 15 states and 16 transitions.
[2025-04-28 21:21:45,564 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:45,564 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 2.0) internal successors, (10), 8 states have internal predecessors, (10), 5 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 5 states have call successors, (5) Word has length 13
[2025-04-28 21:21:45,564 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,565 INFO  L225             Difference]: With dead ends: 15
[2025-04-28 21:21:45,565 INFO  L226             Difference]: Without dead ends: 15
[2025-04-28 21:21:45,565 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 34 GetRequests, 24 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 14 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=34, Invalid=98, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:45,566 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 4 mSDsluCounter, 35 mSDsCounter, 0 mSdLazyCounter, 24 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 46 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 24 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,566 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 46 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 24 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:45,570 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15 states.
[2025-04-28 21:21:45,572 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15 to 15.
[2025-04-28 21:21:45,572 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 15 states, 7 states have (on average 1.1428571428571428) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:45,574 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 15 states to 15 states and 16 transitions.
[2025-04-28 21:21:45,575 INFO  L79                 Accepts]: Start accepts. Automaton has 15 states and 16 transitions. Word has length 13
[2025-04-28 21:21:45,575 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,575 INFO  L485      AbstractCegarLoop]: Abstraction has 15 states and 16 transitions.
[2025-04-28 21:21:45,575 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 2.0) internal successors, (10), 8 states have internal predecessors, (10), 5 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:45,575 INFO  L278                IsEmpty]: Start isEmpty. Operand 15 states and 16 transitions.
[2025-04-28 21:21:45,576 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:45,576 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,576 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,581 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:45,780 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:45,780 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,781 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,781 INFO  L85        PathProgramCache]: Analyzing trace with hash -1486246934, now seen corresponding path program 2 times
[2025-04-28 21:21:45,781 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,781 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1063153107]
[2025-04-28 21:21:45,781 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:45,781 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,800 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:45,825 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:45,825 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:45,825 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,531 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:46,531 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,532 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1063153107]
[2025-04-28 21:21:46,532 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1063153107] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,532 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1448391341]
[2025-04-28 21:21:46,532 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,532 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,535 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,538 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:46,543 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,586 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:46,619 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:46,620 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:46,620 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,623 INFO  L256         TraceCheckSpWp]: Trace formula consists of 129 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,625 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,898 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:46,898 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,116 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:50,116 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1448391341] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,116 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,117 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:50,117 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [657389900]
[2025-04-28 21:21:50,117 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,117 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:50,117 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,118 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:50,118 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=31, Invalid=101, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:50,118 INFO  L87              Difference]: Start difference. First operand 15 states and 16 transitions. Second operand  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:50,311 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,311 INFO  L93              Difference]: Finished difference Result 17 states and 18 transitions.
[2025-04-28 21:21:50,312 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:50,312 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 7 states have call successors, (7) Word has length 17
[2025-04-28 21:21:50,312 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,313 INFO  L225             Difference]: With dead ends: 17
[2025-04-28 21:21:50,313 INFO  L226             Difference]: Without dead ends: 17
[2025-04-28 21:21:50,313 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 45 GetRequests, 30 SyntacticMatches, 1 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 33 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=57, Invalid=183, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:50,314 INFO  L437           NwaCegarLoop]: 12 mSDtfsCounter, 8 mSDsluCounter, 44 mSDsCounter, 0 mSdLazyCounter, 37 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 56 SdHoareTripleChecker+Invalid, 48 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 37 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,314 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 56 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 37 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:50,315 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17 states.
[2025-04-28 21:21:50,317 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 17 to 17.
[2025-04-28 21:21:50,318 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 17 states, 8 states have (on average 1.125) internal successors, (9), 9 states have internal predecessors, (9), 3 states have call successors, (3), 2 states have call predecessors, (3), 5 states have return successors, (6), 5 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:50,318 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 18 transitions.
[2025-04-28 21:21:50,318 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 18 transitions. Word has length 17
[2025-04-28 21:21:50,318 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,319 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 18 transitions.
[2025-04-28 21:21:50,319 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 11 states have internal predecessors, (13), 7 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 4 states have call predecessors, (7), 7 states have call successors, (7)
[2025-04-28 21:21:50,319 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 18 transitions.
[2025-04-28 21:21:50,319 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:50,319 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,319 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,324 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:50,523 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,523 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,524 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,524 INFO  L85        PathProgramCache]: Analyzing trace with hash -2056434034, now seen corresponding path program 3 times
[2025-04-28 21:21:50,524 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,524 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1642694924]
[2025-04-28 21:21:50,524 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:50,524 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,534 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:50,575 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:50,576 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:50,576 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,979 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:51,980 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,980 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1642694924]
[2025-04-28 21:21:51,980 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1642694924] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:51,980 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2027691603]
[2025-04-28 21:21:51,980 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:51,980 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,985 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:51,987 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:51,991 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,054 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:52,102 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:52,102 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:52,102 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,105 INFO  L256         TraceCheckSpWp]: Trace formula consists of 176 conjuncts, 47 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,108 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,790 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:54,790 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:03,881 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:22:03,881 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2027691603] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:03,881 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:03,881 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 21
[2025-04-28 21:22:03,882 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2063765502]
[2025-04-28 21:22:03,882 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:03,882 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 21 states
[2025-04-28 21:22:03,882 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:03,883 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 21 interpolants.
[2025-04-28 21:22:03,884 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=65, Invalid=355, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:22:03,884 INFO  L87              Difference]: Start difference. First operand 17 states and 18 transitions. Second operand  has 21 states, 10 states have (on average 2.2) internal successors, (22), 20 states have internal predecessors, (22), 12 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (12), 8 states have call predecessors, (12), 12 states have call successors, (12)
[2025-04-28 21:22:04,525 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,525 INFO  L93              Difference]: Finished difference Result 19 states and 20 transitions.
[2025-04-28 21:22:04,526 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:04,527 INFO  L79                 Accepts]: Start accepts. Automaton has  has 21 states, 10 states have (on average 2.2) internal successors, (22), 20 states have internal predecessors, (22), 12 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (12), 8 states have call predecessors, (12), 12 states have call successors, (12) Word has length 21
[2025-04-28 21:22:04,527 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,527 INFO  L225             Difference]: With dead ends: 19
[2025-04-28 21:22:04,527 INFO  L226             Difference]: Without dead ends: 19
[2025-04-28 21:22:04,528 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 55 GetRequests, 31 SyntacticMatches, 1 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 118 ImplicationChecksByTransitivity, 1.2s TimeCoverageRelationStatistics Valid=117, Invalid=483, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:22:04,528 INFO  L437           NwaCegarLoop]: 13 mSDtfsCounter, 28 mSDsluCounter, 78 mSDsCounter, 0 mSdLazyCounter, 67 mSolverCounterSat, 34 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 91 SdHoareTripleChecker+Invalid, 101 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 34 IncrementalHoareTripleChecker+Valid, 67 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,529 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 91 Invalid, 101 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [34 Valid, 67 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:04,529 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 19 states.
[2025-04-28 21:22:04,534 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 19 to 19.
[2025-04-28 21:22:04,536 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 19 states, 9 states have (on average 1.1111111111111112) internal successors, (10), 10 states have internal predecessors, (10), 3 states have call successors, (3), 2 states have call predecessors, (3), 6 states have return successors, (7), 6 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:22:04,537 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 19 states to 19 states and 20 transitions.
[2025-04-28 21:22:04,538 INFO  L79                 Accepts]: Start accepts. Automaton has 19 states and 20 transitions. Word has length 21
[2025-04-28 21:22:04,538 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,538 INFO  L485      AbstractCegarLoop]: Abstraction has 19 states and 20 transitions.
[2025-04-28 21:22:04,538 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 21 states, 10 states have (on average 2.2) internal successors, (22), 20 states have internal predecessors, (22), 12 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (12), 8 states have call predecessors, (12), 12 states have call successors, (12)
[2025-04-28 21:22:04,539 INFO  L278                IsEmpty]: Start isEmpty. Operand 19 states and 20 transitions.
[2025-04-28 21:22:04,539 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:22:04,539 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,539 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:04,545 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:22:04,740 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,740 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,740 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,741 INFO  L85        PathProgramCache]: Analyzing trace with hash -434924750, now seen corresponding path program 4 times
[2025-04-28 21:22:04,741 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,741 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [110164826]
[2025-04-28 21:22:04,741 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:04,741 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,751 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:22:04,786 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:04,786 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:22:04,786 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,825 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:22:06,825 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,825 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [110164826]
[2025-04-28 21:22:06,825 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [110164826] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:06,825 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1699641436]
[2025-04-28 21:22:06,825 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:06,826 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,829 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:06,831 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:22:06,834 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:06,929 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:22:06,986 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:22:06,986 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:22:06,986 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,989 INFO  L256         TraceCheckSpWp]: Trace formula consists of 223 conjuncts, 48 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:06,993 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:08,989 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:22:08,989 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
