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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:30,281 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:30,385 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e2c8445b-8eec-44b2-a839-3a757c0cb932/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:30,392 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:30,393 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:30,426 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:30,427 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:30,427 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:30,428 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:30,428 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:30,429 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:30,430 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:30,430 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:30,430 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:30,430 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:30,430 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:30,430 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:30,431 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:30,431 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:30,431 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:30,431 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:30,431 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:30,431 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:30,432 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:30,432 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:30,432 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:30,433 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:30,779 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:30,791 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:30,793 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:30,795 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:30,796 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:30,798 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e2c8445b-8eec-44b2-a839-3a757c0cb932/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-277.smt2
[2025-04-28 21:21:30,800 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:30,809 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:30,972 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e2c8445b-8eec-44b2-a839-3a757c0cb932/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-277.smt2
[2025-04-28 21:21:30,975 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:30,977 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:30,977 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:30,978 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:30,978 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:30,980 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:30" (1/1) ...
[2025-04-28 21:21:31,001 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31 Unit
[2025-04-28 21:21:31,001 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:31,002 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:31,002 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:31,002 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:31,019 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,019 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,043 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,044 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,047 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,048 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,050 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,052 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,052 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,068 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:31,069 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:31,069 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:31,069 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:31,070 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (1/1) ...
[2025-04-28 21:21:31,073 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:31,086 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,101 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:31,105 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:31,115 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:31,115 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:31,115 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:31,115 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure fail given in one single declaration
[2025-04-28 21:21:31,115 INFO  L130     BoogieDeclarations]: Found specification of procedure fail
[2025-04-28 21:21:31,116 INFO  L138     BoogieDeclarations]: Found implementation of procedure fail
[2025-04-28 21:21:31,116 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:31,116 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:31,116 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:31,116 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:31,116 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:31,116 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:31,151 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:31,153 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:31,232 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:31,232 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:31,246 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:31,247 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:31,248 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:31 BoogieIcfgContainer
[2025-04-28 21:21:31,248 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:31,252 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:31,253 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:31,257 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:31,258 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:30" (1/3) ...
[2025-04-28 21:21:31,258 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@42450554 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:31, skipping insertion in model container
[2025-04-28 21:21:31,259 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:31" (2/3) ...
[2025-04-28 21:21:31,259 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@42450554 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:31, skipping insertion in model container
[2025-04-28 21:21:31,260 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:31" (3/3) ...
[2025-04-28 21:21:31,261 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:31,279 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:31,281 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 16 locations, 21 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:31,336 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:31,358 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;@7e20e14a, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:31,358 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:31,363 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4)
[2025-04-28 21:21:31,371 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:31,371 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,372 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,372 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,378 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,379 INFO  L85        PathProgramCache]: Analyzing trace with hash 812378868, now seen corresponding path program 1 times
[2025-04-28 21:21:31,387 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,388 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [414409598]
[2025-04-28 21:21:31,388 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,389 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,424 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:31,434 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:31,434 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,435 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,551 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:31,552 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,552 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [414409598]
[2025-04-28 21:21:31,553 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [414409598] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:31,553 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:31,556 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:31,558 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1843508615]
[2025-04-28 21:21:31,558 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,563 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:31,563 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,594 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:31,594 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:31,597 INFO  L87              Difference]: Start difference. First operand  has 16 states, 7 states have (on average 1.2857142857142858) internal successors, (9), 9 states have internal predecessors, (9), 4 states have call successors, (4), 3 states have call predecessors, (4), 3 states have return successors, (4), 4 states have call predecessors, (4), 4 states have call successors, (4) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:31,649 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,649 INFO  L93              Difference]: Finished difference Result 16 states and 17 transitions.
[2025-04-28 21:21:31,651 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:31,652 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:31,653 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,660 INFO  L225             Difference]: With dead ends: 16
[2025-04-28 21:21:31,660 INFO  L226             Difference]: Without dead ends: 16
[2025-04-28 21:21:31,662 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:31,665 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 1 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 35 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,666 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 35 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:31,685 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 16 states.
[2025-04-28 21:21:31,713 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 16 to 16.
[2025-04-28 21:21:31,717 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 16 states, 7 states have (on average 1.1428571428571428) internal successors, (8), 8 states have internal predecessors, (8), 4 states have call successors, (4), 3 states have call predecessors, (4), 4 states have return successors, (5), 4 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:31,722 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 16 states to 16 states and 17 transitions.
[2025-04-28 21:21:31,723 INFO  L79                 Accepts]: Start accepts. Automaton has 16 states and 17 transitions. Word has length 12
[2025-04-28 21:21:31,724 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,724 INFO  L485      AbstractCegarLoop]: Abstraction has 16 states and 17 transitions.
[2025-04-28 21:21:31,724 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:31,724 INFO  L278                IsEmpty]: Start isEmpty. Operand 16 states and 17 transitions.
[2025-04-28 21:21:31,725 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:31,727 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,727 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:31,727 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:31,727 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,728 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,728 INFO  L85        PathProgramCache]: Analyzing trace with hash 1337627512, now seen corresponding path program 1 times
[2025-04-28 21:21:31,728 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,728 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1970345278]
[2025-04-28 21:21:31,729 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,729 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,742 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:31,763 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:31,767 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,767 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,077 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:32,077 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,077 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1970345278]
[2025-04-28 21:21:32,077 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1970345278] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:32,077 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1321279582]
[2025-04-28 21:21:32,077 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,078 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,080 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:32,083 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:32,088 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:32,130 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:32,145 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:32,145 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,145 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,147 INFO  L256         TraceCheckSpWp]: Trace formula consists of 56 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:32,151 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:32,324 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:32,324 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:32,761 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:32,761 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1321279582] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:32,761 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:32,761 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 11
[2025-04-28 21:21:32,763 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [299312381]
[2025-04-28 21:21:32,763 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,763 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:32,764 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,764 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:32,765 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=29, Invalid=81, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:32,765 INFO  L87              Difference]: Start difference. First operand 16 states and 17 transitions. Second operand  has 11 states, 5 states have (on average 2.6) internal successors, (13), 10 states have internal predecessors, (13), 7 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:32,912 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,913 INFO  L93              Difference]: Finished difference Result 20 states and 21 transitions.
[2025-04-28 21:21:32,914 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:32,914 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 5 states have (on average 2.6) internal successors, (13), 10 states have internal predecessors, (13), 7 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8) Word has length 16
[2025-04-28 21:21:32,915 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,915 INFO  L225             Difference]: With dead ends: 20
[2025-04-28 21:21:32,915 INFO  L226             Difference]: Without dead ends: 20
[2025-04-28 21:21:32,916 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 40 GetRequests, 26 SyntacticMatches, 2 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 20 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=50, Invalid=132, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:32,917 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 9 mSDsluCounter, 54 mSDsCounter, 0 mSdLazyCounter, 25 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 68 SdHoareTripleChecker+Invalid, 37 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 25 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,917 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 68 Invalid, 37 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 25 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:32,918 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 20 states.
[2025-04-28 21:21:32,922 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 20 to 20.
[2025-04-28 21:21:32,923 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 20 states, 9 states have (on average 1.1111111111111112) internal successors, (10), 10 states have internal predecessors, (10), 4 states have call successors, (4), 3 states have call predecessors, (4), 6 states have return successors, (7), 6 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:32,923 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 20 states to 20 states and 21 transitions.
[2025-04-28 21:21:32,924 INFO  L79                 Accepts]: Start accepts. Automaton has 20 states and 21 transitions. Word has length 16
[2025-04-28 21:21:32,924 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,924 INFO  L485      AbstractCegarLoop]: Abstraction has 20 states and 21 transitions.
[2025-04-28 21:21:32,924 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 5 states have (on average 2.6) internal successors, (13), 10 states have internal predecessors, (13), 7 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 3 states have call predecessors, (8), 7 states have call successors, (8)
[2025-04-28 21:21:32,924 INFO  L278                IsEmpty]: Start isEmpty. Operand 20 states and 21 transitions.
[2025-04-28 21:21:32,925 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:32,925 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,925 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,929 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:33,126 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:33,127 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,127 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,131 INFO  L85        PathProgramCache]: Analyzing trace with hash -1097944320, now seen corresponding path program 2 times
[2025-04-28 21:21:33,131 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,131 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1237913102]
[2025-04-28 21:21:33,131 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:33,131 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,157 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:21:33,206 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:33,206 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:33,206 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,456 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:33,456 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,456 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1237913102]
[2025-04-28 21:21:33,456 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1237913102] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,456 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [528029637]
[2025-04-28 21:21:33,456 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:33,457 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,459 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,461 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:33,466 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,499 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 24 statements into 2 equivalence classes.
[2025-04-28 21:21:33,520 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:33,520 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:33,520 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,522 INFO  L256         TraceCheckSpWp]: Trace formula consists of 96 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,523 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,593 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:33,593 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:34,635 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:34,637 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [528029637] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:34,637 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:34,637 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 8, 10] total 15
[2025-04-28 21:21:34,638 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [22684832]
[2025-04-28 21:21:34,638 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,640 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:34,640 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,641 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:34,641 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=55, Invalid=155, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:34,641 INFO  L87              Difference]: Start difference. First operand 20 states and 21 transitions. Second operand  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:34,837 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,840 INFO  L93              Difference]: Finished difference Result 24 states and 25 transitions.
[2025-04-28 21:21:34,840 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:34,840 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 9 states have call successors, (12) Word has length 24
[2025-04-28 21:21:34,841 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,841 INFO  L225             Difference]: With dead ends: 24
[2025-04-28 21:21:34,841 INFO  L226             Difference]: Without dead ends: 24
[2025-04-28 21:21:34,842 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 62 GetRequests, 40 SyntacticMatches, 4 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 59 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=110, Invalid=270, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:34,842 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 18 mSDsluCounter, 50 mSDsCounter, 0 mSdLazyCounter, 28 mSolverCounterSat, 22 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 64 SdHoareTripleChecker+Invalid, 50 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 22 IncrementalHoareTripleChecker+Valid, 28 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,843 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 64 Invalid, 50 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [22 Valid, 28 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:34,843 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 24 states.
[2025-04-28 21:21:34,846 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 24 to 24.
[2025-04-28 21:21:34,847 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 24 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 4 states have call successors, (4), 3 states have call predecessors, (4), 8 states have return successors, (9), 8 states have call predecessors, (9), 4 states have call successors, (9)
[2025-04-28 21:21:34,847 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 24 states to 24 states and 25 transitions.
[2025-04-28 21:21:34,847 INFO  L79                 Accepts]: Start accepts. Automaton has 24 states and 25 transitions. Word has length 24
[2025-04-28 21:21:34,847 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,848 INFO  L485      AbstractCegarLoop]: Abstraction has 24 states and 25 transitions.
[2025-04-28 21:21:34,848 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 14 states have internal predecessors, (17), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:34,848 INFO  L278                IsEmpty]: Start isEmpty. Operand 24 states and 25 transitions.
[2025-04-28 21:21:34,849 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:34,849 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,849 INFO  L218           NwaCegarLoop]: trace histogram [6, 5, 5, 5, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,854 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:35,053 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:35,053 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,054 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,054 INFO  L85        PathProgramCache]: Analyzing trace with hash -627371896, now seen corresponding path program 3 times
[2025-04-28 21:21:35,054 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,054 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [662900521]
[2025-04-28 21:21:35,054 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:35,054 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,062 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 32 statements into 6 equivalence classes.
[2025-04-28 21:21:35,099 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:35,099 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s)
[2025-04-28 21:21:35,099 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,389 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 34 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:21:35,389 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,389 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [662900521]
[2025-04-28 21:21:35,389 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [662900521] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:35,389 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [990853308]
[2025-04-28 21:21:35,389 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:35,390 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:35,392 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,394 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:35,398 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:35,439 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 32 statements into 6 equivalence classes.
[2025-04-28 21:21:35,470 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:35,470 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 6 check-sat command(s)
[2025-04-28 21:21:35,470 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,471 INFO  L256         TraceCheckSpWp]: Trace formula consists of 136 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:35,474 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:35,565 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 30 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:35,565 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:37,801 INFO  L134       CoverageAnalysis]: Checked inductivity of 55 backedges. 0 proven. 40 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:37,801 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [990853308] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:37,802 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:37,802 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 10, 14] total 19
[2025-04-28 21:21:37,802 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1150659233]
[2025-04-28 21:21:37,802 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,802 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:37,802 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,805 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:37,805 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=89, Invalid=253, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:37,806 INFO  L87              Difference]: Start difference. First operand 24 states and 25 transitions. Second operand  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:38,045 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,045 INFO  L93              Difference]: Finished difference Result 28 states and 29 transitions.
[2025-04-28 21:21:38,046 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:38,047 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16) Word has length 32
[2025-04-28 21:21:38,047 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,048 INFO  L225             Difference]: With dead ends: 28
[2025-04-28 21:21:38,048 INFO  L226             Difference]: Without dead ends: 28
[2025-04-28 21:21:38,048 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 84 GetRequests, 54 SyntacticMatches, 6 SemanticMatches, 24 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 125 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=194, Invalid=456, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:38,049 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 22 mSDsluCounter, 87 mSDsCounter, 0 mSdLazyCounter, 44 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 23 SdHoareTripleChecker+Valid, 101 SdHoareTripleChecker+Invalid, 70 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 44 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,049 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [23 Valid, 101 Invalid, 70 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 44 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:38,053 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 28 states.
[2025-04-28 21:21:38,059 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 28 to 28.
[2025-04-28 21:21:38,059 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 28 states, 13 states have (on average 1.0769230769230769) internal successors, (14), 14 states have internal predecessors, (14), 4 states have call successors, (4), 3 states have call predecessors, (4), 10 states have return successors, (11), 10 states have call predecessors, (11), 4 states have call successors, (11)
[2025-04-28 21:21:38,061 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 28 states to 28 states and 29 transitions.
[2025-04-28 21:21:38,061 INFO  L79                 Accepts]: Start accepts. Automaton has 28 states and 29 transitions. Word has length 32
[2025-04-28 21:21:38,062 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,062 INFO  L485      AbstractCegarLoop]: Abstraction has 28 states and 29 transitions.
[2025-04-28 21:21:38,063 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 18 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:21:38,064 INFO  L278                IsEmpty]: Start isEmpty. Operand 28 states and 29 transitions.
[2025-04-28 21:21:38,064 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 41
[2025-04-28 21:21:38,065 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,065 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,071 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:38,268 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,268 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,269 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,269 INFO  L85        PathProgramCache]: Analyzing trace with hash -1020351472, now seen corresponding path program 4 times
[2025-04-28 21:21:38,269 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,269 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [693717126]
[2025-04-28 21:21:38,269 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:38,269 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,276 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 40 statements into 2 equivalence classes.
[2025-04-28 21:21:38,305 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:38,305 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:38,306 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,647 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 62 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:38,648 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,648 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [693717126]
[2025-04-28 21:21:38,648 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [693717126] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:38,648 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1113109667]
[2025-04-28 21:21:38,648 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:38,648 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,650 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:38,653 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:38,658 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:38,722 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 40 statements into 2 equivalence classes.
[2025-04-28 21:21:38,749 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s) and asserted 40 of 40 statements.
[2025-04-28 21:21:38,749 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 1 check-sat command(s)
[2025-04-28 21:21:38,750 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,751 INFO  L256         TraceCheckSpWp]: Trace formula consists of 176 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:38,753 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:38,855 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 56 refuted. 0 times theorem prover too weak. 49 trivial. 0 not checked.
[2025-04-28 21:21:38,855 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:42,909 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 77 refuted. 0 times theorem prover too weak. 28 trivial. 0 not checked.
[2025-04-28 21:21:42,909 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1113109667] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:42,909 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:42,910 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 12, 18] total 23
[2025-04-28 21:21:42,910 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2073191530]
[2025-04-28 21:21:42,910 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,910 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:42,910 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,911 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:42,912 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=131, Invalid=375, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:42,912 INFO  L87              Difference]: Start difference. First operand 28 states and 29 transitions. Second operand  has 23 states, 11 states have (on average 2.272727272727273) internal successors, (25), 22 states have internal predecessors, (25), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (20), 9 states have call predecessors, (20), 13 states have call successors, (20)
[2025-04-28 21:21:43,173 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,173 INFO  L93              Difference]: Finished difference Result 32 states and 33 transitions.
[2025-04-28 21:21:43,174 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:43,174 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 11 states have (on average 2.272727272727273) internal successors, (25), 22 states have internal predecessors, (25), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (20), 9 states have call predecessors, (20), 13 states have call successors, (20) Word has length 40
[2025-04-28 21:21:43,174 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,175 INFO  L225             Difference]: With dead ends: 32
[2025-04-28 21:21:43,175 INFO  L226             Difference]: Without dead ends: 32
[2025-04-28 21:21:43,176 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 106 GetRequests, 68 SyntacticMatches, 8 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 215 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=302, Invalid=690, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:43,178 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 26 mSDsluCounter, 97 mSDsCounter, 0 mSdLazyCounter, 46 mSolverCounterSat, 29 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 27 SdHoareTripleChecker+Valid, 111 SdHoareTripleChecker+Invalid, 75 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 29 IncrementalHoareTripleChecker+Valid, 46 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,179 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [27 Valid, 111 Invalid, 75 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [29 Valid, 46 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:43,180 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 32 states.
[2025-04-28 21:21:43,185 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 32 to 32.
[2025-04-28 21:21:43,186 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 15 states have (on average 1.0666666666666667) internal successors, (16), 16 states have internal predecessors, (16), 4 states have call successors, (4), 3 states have call predecessors, (4), 12 states have return successors, (13), 12 states have call predecessors, (13), 4 states have call successors, (13)
[2025-04-28 21:21:43,187 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 33 transitions.
[2025-04-28 21:21:43,187 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 33 transitions. Word has length 40
[2025-04-28 21:21:43,187 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,187 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 33 transitions.
[2025-04-28 21:21:43,187 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 11 states have (on average 2.272727272727273) internal successors, (25), 22 states have internal predecessors, (25), 13 states have call successors, (14), 1 states have call predecessors, (14), 10 states have return successors, (20), 9 states have call predecessors, (20), 13 states have call successors, (20)
[2025-04-28 21:21:43,187 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 33 transitions.
[2025-04-28 21:21:43,188 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 49
[2025-04-28 21:21:43,189 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,189 INFO  L218           NwaCegarLoop]: trace histogram [10, 9, 9, 9, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,194 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:43,392 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable5
[2025-04-28 21:21:43,393 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,393 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,393 INFO  L85        PathProgramCache]: Analyzing trace with hash -635927144, now seen corresponding path program 5 times
[2025-04-28 21:21:43,393 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,393 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [572476531]
[2025-04-28 21:21:43,393 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:43,394 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,402 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 48 statements into 10 equivalence classes.
[2025-04-28 21:21:43,571 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 10 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:43,571 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 10 check-sat command(s)
[2025-04-28 21:21:43,571 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,992 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 8 proven. 90 refuted. 0 times theorem prover too weak. 73 trivial. 0 not checked.
[2025-04-28 21:21:43,992 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,992 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [572476531]
[2025-04-28 21:21:43,992 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [572476531] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,992 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1174369661]
[2025-04-28 21:21:43,992 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:43,992 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,995 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,997 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:44,001 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,107 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 48 statements into 10 equivalence classes.
[2025-04-28 21:21:44,148 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 10 check-sat command(s) and asserted 48 of 48 statements.
[2025-04-28 21:21:44,148 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 10 check-sat command(s)
[2025-04-28 21:21:44,148 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,149 INFO  L256         TraceCheckSpWp]: Trace formula consists of 216 conjuncts, 21 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,151 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,232 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 90 refuted. 0 times theorem prover too weak. 81 trivial. 0 not checked.
[2025-04-28 21:21:44,233 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,888 INFO  L134       CoverageAnalysis]: Checked inductivity of 171 backedges. 0 proven. 126 refuted. 0 times theorem prover too weak. 45 trivial. 0 not checked.
[2025-04-28 21:21:50,888 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1174369661] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,888 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,888 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [15, 14, 22] total 26
[2025-04-28 21:21:50,889 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [656433325]
[2025-04-28 21:21:50,889 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,889 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 26 states
[2025-04-28 21:21:50,889 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,890 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 26 interpolants.
[2025-04-28 21:21:50,891 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=181, Invalid=469, Unknown=0, NotChecked=0, Total=650
[2025-04-28 21:21:50,891 INFO  L87              Difference]: Start difference. First operand 32 states and 33 transitions. Second operand  has 26 states, 13 states have (on average 2.1538461538461537) internal successors, (28), 25 states have internal predecessors, (28), 14 states have call successors, (15), 1 states have call predecessors, (15), 12 states have return successors, (23), 11 states have call predecessors, (23), 14 states have call successors, (23)
[2025-04-28 21:21:51,096 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,096 INFO  L93              Difference]: Finished difference Result 34 states and 35 transitions.
[2025-04-28 21:21:51,096 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 14 states. 
[2025-04-28 21:21:51,097 INFO  L79                 Accepts]: Start accepts. Automaton has  has 26 states, 13 states have (on average 2.1538461538461537) internal successors, (28), 25 states have internal predecessors, (28), 14 states have call successors, (15), 1 states have call predecessors, (15), 12 states have return successors, (23), 11 states have call predecessors, (23), 14 states have call successors, (23) Word has length 48
[2025-04-28 21:21:51,097 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,098 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:51,098 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:51,098 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 126 GetRequests, 82 SyntacticMatches, 11 SemanticMatches, 33 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 418 ImplicationChecksByTransitivity, 0.5s TimeCoverageRelationStatistics Valid=388, Invalid=802, Unknown=0, NotChecked=0, Total=1190
[2025-04-28 21:21:51,099 INFO  L437           NwaCegarLoop]: 14 mSDtfsCounter, 48 mSDsluCounter, 111 mSDsCounter, 0 mSdLazyCounter, 56 mSolverCounterSat, 45 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 60 SdHoareTripleChecker+Valid, 125 SdHoareTripleChecker+Invalid, 101 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 45 IncrementalHoareTripleChecker+Valid, 56 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,100 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [60 Valid, 125 Invalid, 101 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [45 Valid, 56 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:51,100 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:51,104 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 34.
[2025-04-28 21:21:51,104 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 34 states, 16 states have (on average 1.0625) internal successors, (17), 17 states have internal predecessors, (17), 4 states have call successors, (4), 3 states have call predecessors, (4), 13 states have return successors, (14), 13 states have call predecessors, (14), 4 states have call successors, (14)
[2025-04-28 21:21:51,105 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 34 states to 34 states and 35 transitions.
[2025-04-28 21:21:51,105 INFO  L79                 Accepts]: Start accepts. Automaton has 34 states and 35 transitions. Word has length 48
[2025-04-28 21:21:51,105 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,105 INFO  L485      AbstractCegarLoop]: Abstraction has 34 states and 35 transitions.
[2025-04-28 21:21:51,105 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 26 states, 13 states have (on average 2.1538461538461537) internal successors, (28), 25 states have internal predecessors, (28), 14 states have call successors, (15), 1 states have call predecessors, (15), 12 states have return successors, (23), 11 states have call predecessors, (23), 14 states have call successors, (23)
[2025-04-28 21:21:51,105 INFO  L278                IsEmpty]: Start isEmpty. Operand 34 states and 35 transitions.
[2025-04-28 21:21:51,106 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 53
[2025-04-28 21:21:51,107 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,107 INFO  L218           NwaCegarLoop]: trace histogram [11, 10, 10, 10, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,113 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:51,307 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,307 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,308 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,308 INFO  L85        PathProgramCache]: Analyzing trace with hash -722634340, now seen corresponding path program 6 times
[2025-04-28 21:21:51,308 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,308 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [927351261]
[2025-04-28 21:21:51,308 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:51,308 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,329 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 52 statements into 11 equivalence classes.
[2025-04-28 21:21:51,467 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:51,467 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s)
[2025-04-28 21:21:51,467 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,712 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 14 proven. 140 refuted. 0 times theorem prover too weak. 56 trivial. 0 not checked.
[2025-04-28 21:21:54,712 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,712 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [927351261]
[2025-04-28 21:21:54,712 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [927351261] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,712 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1290806907]
[2025-04-28 21:21:54,712 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:21:54,713 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,715 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,717 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:54,720 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,900 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 52 statements into 11 equivalence classes.
[2025-04-28 21:21:54,974 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s) and asserted 52 of 52 statements.
[2025-04-28 21:21:54,974 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 11 check-sat command(s)
[2025-04-28 21:21:54,974 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,981 WARN  L254         TraceCheckSpWp]: Trace formula consists of 236 conjuncts, 167 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,985 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,695 INFO  L134       CoverageAnalysis]: Checked inductivity of 210 backedges. 21 proven. 113 refuted. 0 times theorem prover too weak. 76 trivial. 0 not checked.
[2025-04-28 21:21:56,695 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
