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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:51,251 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:51,339 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53f5688f-4dad-4bdd-ad95-e6935564fcff/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:51,346 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:51,346 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:51,373 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:51,373 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:51,374 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:51,374 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:51,374 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:51,375 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:51,375 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:51,375 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:51,375 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:51,375 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:51,375 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:51,375 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:51,376 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:51,376 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:51,376 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:51,376 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:51,376 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:51,376 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:51,377 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:51,377 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:51,378 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:51,378 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:51,743 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:51,758 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:51,761 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:51,764 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:51,764 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:51,765 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53f5688f-4dad-4bdd-ad95-e6935564fcff/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-072.smt2
[2025-04-28 21:21:51,768 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:51,771 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:51,912 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_53f5688f-4dad-4bdd-ad95-e6935564fcff/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-072.smt2
[2025-04-28 21:21:51,918 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:51,921 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:51,921 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:51,921 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:51,922 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:51,924 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,947 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51 Unit
[2025-04-28 21:21:51,948 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:51,949 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:51,949 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:51,951 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:51,967 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,967 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,998 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:51,998 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:52,002 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:52,005 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:52,006 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:52,007 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:52,008 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:52,025 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:52,026 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:52,026 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:52,026 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:52,027 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (1/1) ...
[2025-04-28 21:21:52,031 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:52,049 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,066 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:52,070 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:52,091 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:52,091 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:52,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:52,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:52,092 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:52,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:52,092 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:52,092 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:52,092 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:52,135 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:52,138 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:52,205 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:52,205 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:52,218 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:52,219 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:52,220 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:52 BoogieIcfgContainer
[2025-04-28 21:21:52,220 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:52,223 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:52,223 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:52,229 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:52,229 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:51" (1/3) ...
[2025-04-28 21:21:52,230 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@75c0a6b2 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:52, skipping insertion in model container
[2025-04-28 21:21:52,231 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:51" (2/3) ...
[2025-04-28 21:21:52,233 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@75c0a6b2 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:52, skipping insertion in model container
[2025-04-28 21:21:52,233 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:52" (3/3) ...
[2025-04-28 21:21:52,234 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:52,253 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:52,255 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:52,303 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:52,318 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;@13ec1bd2, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:52,318 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:52,323 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:52,337 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:52,337 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,338 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,338 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,345 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,346 INFO  L85        PathProgramCache]: Analyzing trace with hash -1586659766, now seen corresponding path program 1 times
[2025-04-28 21:21:52,356 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,357 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1779119268]
[2025-04-28 21:21:52,357 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,359 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,387 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:52,405 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:52,405 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,405 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,526 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:52,527 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,528 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1779119268]
[2025-04-28 21:21:52,531 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1779119268] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:52,531 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:52,537 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:52,539 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1816465529]
[2025-04-28 21:21:52,540 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,545 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:52,545 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,591 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:52,591 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:52,594 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:52,646 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,647 INFO  L93              Difference]: Finished difference Result 13 states and 14 transitions.
[2025-04-28 21:21:52,648 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:52,650 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:52,650 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,659 INFO  L225             Difference]: With dead ends: 13
[2025-04-28 21:21:52,660 INFO  L226             Difference]: Without dead ends: 13
[2025-04-28 21:21:52,664 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:52,669 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:52,670 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:52,687 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 13 states.
[2025-04-28 21:21:52,707 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 13 to 13.
[2025-04-28 21:21:52,708 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:52,712 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 13 states to 13 states and 14 transitions.
[2025-04-28 21:21:52,713 INFO  L79                 Accepts]: Start accepts. Automaton has 13 states and 14 transitions. Word has length 9
[2025-04-28 21:21:52,713 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,713 INFO  L485      AbstractCegarLoop]: Abstraction has 13 states and 14 transitions.
[2025-04-28 21:21:52,713 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:52,714 INFO  L278                IsEmpty]: Start isEmpty. Operand 13 states and 14 transitions.
[2025-04-28 21:21:52,715 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:52,715 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,715 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,716 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:52,716 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,716 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,717 INFO  L85        PathProgramCache]: Analyzing trace with hash 1339989006, now seen corresponding path program 1 times
[2025-04-28 21:21:52,717 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,717 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1842030673]
[2025-04-28 21:21:52,717 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,717 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,723 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:52,735 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:52,736 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,736 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,902 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:52,902 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,902 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1842030673]
[2025-04-28 21:21:52,902 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1842030673] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,903 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [768932948]
[2025-04-28 21:21:52,903 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,903 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,906 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,911 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:52,913 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,968 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:52,994 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:52,994 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,994 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,997 INFO  L256         TraceCheckSpWp]: Trace formula consists of 36 conjuncts, 5 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,006 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,134 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:53,135 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,516 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:53,517 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [768932948] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,517 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,517 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 8
[2025-04-28 21:21:53,518 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1609527150]
[2025-04-28 21:21:53,518 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,519 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:53,519 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,520 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:53,520 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=18, Invalid=38, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:53,520 INFO  L87              Difference]: Start difference. First operand 13 states and 14 transitions. Second operand  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:53,595 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,595 INFO  L93              Difference]: Finished difference Result 15 states and 16 transitions.
[2025-04-28 21:21:53,597 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:53,598 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5) Word has length 13
[2025-04-28 21:21:53,598 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,598 INFO  L225             Difference]: With dead ends: 15
[2025-04-28 21:21:53,599 INFO  L226             Difference]: Without dead ends: 15
[2025-04-28 21:21:53,599 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 32 GetRequests, 23 SyntacticMatches, 2 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 7 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=23, Invalid=49, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:53,600 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 5 mSDsluCounter, 21 mSDsCounter, 0 mSdLazyCounter, 16 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 32 SdHoareTripleChecker+Invalid, 19 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 16 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,600 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 32 Invalid, 19 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 16 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:53,603 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 15 states.
[2025-04-28 21:21:53,605 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 15 to 15.
[2025-04-28 21:21:53,606 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:53,608 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 15 states to 15 states and 16 transitions.
[2025-04-28 21:21:53,608 INFO  L79                 Accepts]: Start accepts. Automaton has 15 states and 16 transitions. Word has length 13
[2025-04-28 21:21:53,609 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,609 INFO  L485      AbstractCegarLoop]: Abstraction has 15 states and 16 transitions.
[2025-04-28 21:21:53,609 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.25) internal successors, (9), 7 states have internal predecessors, (9), 5 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 5 states have call successors, (5)
[2025-04-28 21:21:53,609 INFO  L278                IsEmpty]: Start isEmpty. Operand 15 states and 16 transitions.
[2025-04-28 21:21:53,610 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:53,610 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,610 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,616 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:53,814 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:53,815 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,815 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,816 INFO  L85        PathProgramCache]: Analyzing trace with hash -1013855662, now seen corresponding path program 2 times
[2025-04-28 21:21:53,816 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,816 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1851978476]
[2025-04-28 21:21:53,816 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:53,816 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,827 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:53,839 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:53,839 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:53,839 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,044 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:54,045 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,045 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1851978476]
[2025-04-28 21:21:54,045 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1851978476] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,045 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1923815773]
[2025-04-28 21:21:54,045 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:54,045 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,049 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,051 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:54,054 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,091 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 17 statements into 2 equivalence classes.
[2025-04-28 21:21:54,106 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:54,106 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:54,106 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,107 INFO  L256         TraceCheckSpWp]: Trace formula consists of 48 conjuncts, 7 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,108 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,158 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:54,158 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:54,668 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:54,669 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1923815773] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:54,669 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:54,669 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 8] total 10
[2025-04-28 21:21:54,669 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1665659730]
[2025-04-28 21:21:54,669 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,670 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:54,670 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,670 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:54,672 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:54,673 INFO  L87              Difference]: Start difference. First operand 15 states and 16 transitions. Second operand  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:54,744 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,746 INFO  L93              Difference]: Finished difference Result 17 states and 18 transitions.
[2025-04-28 21:21:54,747 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:54,747 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 17
[2025-04-28 21:21:54,747 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,747 INFO  L225             Difference]: With dead ends: 17
[2025-04-28 21:21:54,748 INFO  L226             Difference]: Without dead ends: 17
[2025-04-28 21:21:54,749 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 43 GetRequests, 30 SyntacticMatches, 3 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=42, Invalid=90, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:54,750 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 8 mSDsluCounter, 22 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 33 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,751 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 33 Invalid, 26 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:54,753 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17 states.
[2025-04-28 21:21:54,758 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 17 to 17.
[2025-04-28 21:21:54,759 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:54,759 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 18 transitions.
[2025-04-28 21:21:54,762 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 18 transitions. Word has length 17
[2025-04-28 21:21:54,762 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,762 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 18 transitions.
[2025-04-28 21:21:54,762 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.2) internal successors, (11), 9 states have internal predecessors, (11), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:54,762 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 18 transitions.
[2025-04-28 21:21:54,763 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:54,763 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,763 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,768 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:54,963 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:54,964 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,964 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,964 INFO  L85        PathProgramCache]: Analyzing trace with hash 447752470, now seen corresponding path program 3 times
[2025-04-28 21:21:54,965 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,965 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [151078846]
[2025-04-28 21:21:54,965 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:54,965 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,971 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:54,989 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:54,989 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:54,989 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,147 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:55,147 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,147 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [151078846]
[2025-04-28 21:21:55,147 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [151078846] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,147 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1165157291]
[2025-04-28 21:21:55,147 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:55,147 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,150 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,153 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:55,156 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:55,192 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 21 statements into 4 equivalence classes.
[2025-04-28 21:21:55,211 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:55,211 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 4 check-sat command(s)
[2025-04-28 21:21:55,211 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,213 INFO  L256         TraceCheckSpWp]: Trace formula consists of 60 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:55,214 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:55,273 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:55,273 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:56,068 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:56,069 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1165157291] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:56,069 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:56,069 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 10] total 12
[2025-04-28 21:21:56,069 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1755826862]
[2025-04-28 21:21:56,069 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:56,069 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:56,070 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:56,071 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:56,072 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=40, Invalid=92, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:56,073 INFO  L87              Difference]: Start difference. First operand 17 states and 18 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, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:56,164 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,164 INFO  L93              Difference]: Finished difference Result 19 states and 20 transitions.
[2025-04-28 21:21:56,169 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:56,169 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, (9), 4 states have call predecessors, (9), 7 states have call successors, (9) Word has length 21
[2025-04-28 21:21:56,169 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,170 INFO  L225             Difference]: With dead ends: 19
[2025-04-28 21:21:56,170 INFO  L226             Difference]: Without dead ends: 19
[2025-04-28 21:21:56,170 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 54 GetRequests, 37 SyntacticMatches, 4 SemanticMatches, 13 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 35 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=67, Invalid=143, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:56,171 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 10 mSDsluCounter, 46 mSDsCounter, 0 mSdLazyCounter, 32 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 57 SdHoareTripleChecker+Invalid, 39 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 32 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,171 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 57 Invalid, 39 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 32 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:56,172 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 19 states.
[2025-04-28 21:21:56,176 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 19 to 19.
[2025-04-28 21:21:56,177 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:21:56,177 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 19 states to 19 states and 20 transitions.
[2025-04-28 21:21:56,177 INFO  L79                 Accepts]: Start accepts. Automaton has 19 states and 20 transitions. Word has length 21
[2025-04-28 21:21:56,178 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,178 INFO  L485      AbstractCegarLoop]: Abstraction has 19 states and 20 transitions.
[2025-04-28 21:21:56,178 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, (9), 4 states have call predecessors, (9), 7 states have call successors, (9)
[2025-04-28 21:21:56,178 INFO  L278                IsEmpty]: Start isEmpty. Operand 19 states and 20 transitions.
[2025-04-28 21:21:56,179 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:56,179 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,179 INFO  L218           NwaCegarLoop]: trace histogram [5, 4, 4, 4, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,184 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:56,379 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:56,380 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,380 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,380 INFO  L85        PathProgramCache]: Analyzing trace with hash -436545446, now seen corresponding path program 4 times
[2025-04-28 21:21:56,380 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,380 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1345379418]
[2025-04-28 21:21:56,380 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:56,380 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,387 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:56,395 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:56,396 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:56,396 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,728 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 2 proven. 23 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:56,728 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:56,728 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1345379418]
[2025-04-28 21:21:56,728 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1345379418] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:56,728 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1671526291]
[2025-04-28 21:21:56,728 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:56,728 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,731 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:56,733 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:56,736 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,773 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:56,787 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:56,787 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:56,787 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,788 INFO  L256         TraceCheckSpWp]: Trace formula consists of 72 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,790 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,904 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:56,905 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,042 INFO  L134       CoverageAnalysis]: Checked inductivity of 36 backedges. 0 proven. 26 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:58,043 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1671526291] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:58,043 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:58,043 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [11, 9, 12] total 20
[2025-04-28 21:21:58,043 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1372343652]
[2025-04-28 21:21:58,043 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,044 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 20 states
[2025-04-28 21:21:58,044 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,045 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 20 interpolants.
[2025-04-28 21:21:58,046 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=94, Invalid=286, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:58,046 INFO  L87              Difference]: Start difference. First operand 19 states and 20 transitions. Second operand  has 20 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 19 states have internal predecessors, (22), 12 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (16), 6 states have call predecessors, (16), 12 states have call successors, (16)
[2025-04-28 21:21:58,217 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:58,219 INFO  L93              Difference]: Finished difference Result 23 states and 24 transitions.
[2025-04-28 21:21:58,220 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:58,220 INFO  L79                 Accepts]: Start accepts. Automaton has  has 20 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 19 states have internal predecessors, (22), 12 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (16), 6 states have call predecessors, (16), 12 states have call successors, (16) Word has length 25
[2025-04-28 21:21:58,220 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:58,221 INFO  L225             Difference]: With dead ends: 23
[2025-04-28 21:21:58,221 INFO  L226             Difference]: Without dead ends: 23
[2025-04-28 21:21:58,221 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 38 SyntacticMatches, 5 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 172 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=169, Invalid=431, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:21:58,222 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 26 mSDsluCounter, 81 mSDsCounter, 0 mSdLazyCounter, 57 mSolverCounterSat, 23 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 92 SdHoareTripleChecker+Invalid, 80 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 23 IncrementalHoareTripleChecker+Valid, 57 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:58,224 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 92 Invalid, 80 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [23 Valid, 57 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:58,225 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 23 states.
[2025-04-28 21:21:58,231 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 23 to 23.
[2025-04-28 21:21:58,231 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 23 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 3 states have call successors, (3), 2 states have call predecessors, (3), 8 states have return successors, (9), 8 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:58,232 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 23 states to 23 states and 24 transitions.
[2025-04-28 21:21:58,232 INFO  L79                 Accepts]: Start accepts. Automaton has 23 states and 24 transitions. Word has length 25
[2025-04-28 21:21:58,232 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:58,232 INFO  L485      AbstractCegarLoop]: Abstraction has 23 states and 24 transitions.
[2025-04-28 21:21:58,232 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 20 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 19 states have internal predecessors, (22), 12 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (16), 6 states have call predecessors, (16), 12 states have call successors, (16)
[2025-04-28 21:21:58,233 INFO  L278                IsEmpty]: Start isEmpty. Operand 23 states and 24 transitions.
[2025-04-28 21:21:58,236 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:58,236 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:58,236 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:58,241 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:58,440 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:58,440 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,441 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,441 INFO  L85        PathProgramCache]: Analyzing trace with hash 353478754, now seen corresponding path program 5 times
[2025-04-28 21:21:58,441 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,441 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1392944476]
[2025-04-28 21:21:58,441 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:58,441 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,447 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:58,465 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:58,466 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:58,466 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,693 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 3 proven. 44 refuted. 0 times theorem prover too weak. 31 trivial. 0 not checked.
[2025-04-28 21:21:58,693 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,694 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1392944476]
[2025-04-28 21:21:58,694 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1392944476] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,694 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1607985180]
[2025-04-28 21:21:58,694 INFO  L95    rtionOrderModulation]: Changing assertion order to INSIDE_LOOP_FIRST1
[2025-04-28 21:21:58,694 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,697 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:58,699 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:58,702 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,751 INFO  L108    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:58,775 INFO  L111    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:58,775 INFO  L114    AnnotateAndAsserter]: Assert order INSIDE_LOOP_FIRST1 issued 7 check-sat command(s)
[2025-04-28 21:21:58,775 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,777 INFO  L256         TraceCheckSpWp]: Trace formula consists of 96 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,779 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,840 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 42 refuted. 0 times theorem prover too weak. 36 trivial. 0 not checked.
[2025-04-28 21:21:58,840 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,073 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 57 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:22:01,073 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1607985180] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,074 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,074 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 11, 16] total 19
[2025-04-28 21:22:01,074 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [222148933]
[2025-04-28 21:22:01,074 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,075 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:22:01,075 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,076 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:22:01,078 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=97, Invalid=245, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:22:01,078 INFO  L87              Difference]: Start difference. First operand 23 states and 24 transitions. Second operand  has 19 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 18 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:22:01,184 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,184 INFO  L93              Difference]: Finished difference Result 25 states and 26 transitions.
[2025-04-28 21:22:01,185 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:01,186 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 18 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16) Word has length 33
[2025-04-28 21:22:01,186 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,186 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:22:01,186 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:22:01,187 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 87 GetRequests, 57 SyntacticMatches, 7 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 149 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=193, Invalid=407, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:22:01,188 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 9 mSDsluCounter, 60 mSDsCounter, 0 mSdLazyCounter, 42 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 71 SdHoareTripleChecker+Invalid, 44 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 42 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,188 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 71 Invalid, 44 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 42 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:22:01,189 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:22:01,192 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 25.
[2025-04-28 21:22:01,192 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 25 states, 12 states have (on average 1.0833333333333333) internal successors, (13), 13 states have internal predecessors, (13), 3 states have call successors, (3), 2 states have call predecessors, (3), 9 states have return successors, (10), 9 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:22:01,193 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 26 transitions.
[2025-04-28 21:22:01,193 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 26 transitions. Word has length 33
[2025-04-28 21:22:01,193 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,193 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 26 transitions.
[2025-04-28 21:22:01,193 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.2222222222222223) internal successors, (20), 18 states have internal predecessors, (20), 11 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (16), 7 states have call predecessors, (16), 11 states have call successors, (16)
[2025-04-28 21:22:01,194 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 26 transitions.
[2025-04-28 21:22:01,194 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:22:01,194 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,195 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,198 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:22:01,395 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,396 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,396 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,396 INFO  L85        PathProgramCache]: Analyzing trace with hash 827853094, now seen corresponding path program 6 times
[2025-04-28 21:22:01,396 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,396 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [86874935]
[2025-04-28 21:22:01,396 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:22:01,396 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,402 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 37 statements into 8 equivalence classes.
[2025-04-28 21:22:01,419 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:22:01,422 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s)
[2025-04-28 21:22:01,422 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,264 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 1 proven. 75 refuted. 0 times theorem prover too weak. 29 trivial. 0 not checked.
[2025-04-28 21:22:02,264 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,264 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [86874935]
[2025-04-28 21:22:02,264 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [86874935] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,264 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [647667131]
[2025-04-28 21:22:02,265 INFO  L95    rtionOrderModulation]: Changing assertion order to MIX_INSIDE_OUTSIDE
[2025-04-28 21:22:02,265 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,267 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:02,269 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:22:02,272 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,348 INFO  L108    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE partitioned 37 statements into 8 equivalence classes.
[2025-04-28 21:22:02,370 INFO  L111    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:22:02,370 INFO  L114    AnnotateAndAsserter]: Assert order MIX_INSIDE_OUTSIDE issued 8 check-sat command(s)
[2025-04-28 21:22:02,370 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,371 INFO  L256         TraceCheckSpWp]: Trace formula consists of 108 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,373 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:02,657 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:22:02,657 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:05,813 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:22:05,814 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [647667131] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:05,814 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:05,814 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [17, 12, 18] total 35
[2025-04-28 21:22:05,814 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [425592659]
[2025-04-28 21:22:05,814 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:05,815 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 35 states
[2025-04-28 21:22:05,815 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:05,816 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 35 interpolants.
[2025-04-28 21:22:05,816 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=237, Invalid=953, Unknown=0, NotChecked=0, Total=1190
[2025-04-28 21:22:05,817 INFO  L87              Difference]: Start difference. First operand 25 states and 26 transitions. Second operand  has 35 states, 18 states have (on average 2.0555555555555554) internal successors, (37), 34 states have internal predecessors, (37), 18 states have call successors, (18), 1 states have call predecessors, (18), 17 states have return successors, (25), 15 states have call predecessors, (25), 18 states have call successors, (25)
[2025-04-28 21:22:06,777 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,777 INFO  L93              Difference]: Finished difference Result 39 states and 40 transitions.
[2025-04-28 21:22:06,778 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 18 states. 
[2025-04-28 21:22:06,778 INFO  L79                 Accepts]: Start accepts. Automaton has  has 35 states, 18 states have (on average 2.0555555555555554) internal successors, (37), 34 states have internal predecessors, (37), 18 states have call successors, (18), 1 states have call predecessors, (18), 17 states have return successors, (25), 15 states have call predecessors, (25), 18 states have call successors, (25) Word has length 37
[2025-04-28 21:22:06,778 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,779 INFO  L225             Difference]: With dead ends: 39
[2025-04-28 21:22:06,779 INFO  L226             Difference]: Without dead ends: 39
[2025-04-28 21:22:06,780 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 105 GetRequests, 50 SyntacticMatches, 8 SemanticMatches, 47 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 620 ImplicationChecksByTransitivity, 1.5s TimeCoverageRelationStatistics Valid=636, Invalid=1716, Unknown=0, NotChecked=0, Total=2352
[2025-04-28 21:22:06,781 INFO  L437           NwaCegarLoop]: 12 mSDtfsCounter, 87 mSDsluCounter, 124 mSDsCounter, 0 mSdLazyCounter, 92 mSolverCounterSat, 99 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 88 SdHoareTripleChecker+Valid, 136 SdHoareTripleChecker+Invalid, 191 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 99 IncrementalHoareTripleChecker+Valid, 92 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,781 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [88 Valid, 136 Invalid, 191 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [99 Valid, 92 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:06,782 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 39 states.
[2025-04-28 21:22:06,786 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 39 to 39.
[2025-04-28 21:22:06,786 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 39 states, 19 states have (on average 1.0526315789473684) internal successors, (20), 20 states have internal predecessors, (20), 3 states have call successors, (3), 2 states have call predecessors, (3), 16 states have return successors, (17), 16 states have call predecessors, (17), 3 states have call successors, (17)
[2025-04-28 21:22:06,787 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 39 states to 39 states and 40 transitions.
[2025-04-28 21:22:06,787 INFO  L79                 Accepts]: Start accepts. Automaton has 39 states and 40 transitions. Word has length 37
[2025-04-28 21:22:06,787 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,787 INFO  L485      AbstractCegarLoop]: Abstraction has 39 states and 40 transitions.
[2025-04-28 21:22:06,788 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 35 states, 18 states have (on average 2.0555555555555554) internal successors, (37), 34 states have internal predecessors, (37), 18 states have call successors, (18), 1 states have call predecessors, (18), 17 states have return successors, (25), 15 states have call predecessors, (25), 18 states have call successors, (25)
[2025-04-28 21:22:06,788 INFO  L278                IsEmpty]: Start isEmpty. Operand 39 states and 40 transitions.
[2025-04-28 21:22:06,789 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 66
[2025-04-28 21:22:06,789 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,789 INFO  L218           NwaCegarLoop]: trace histogram [15, 14, 14, 14, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:06,793 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:22:06,990 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:06,990 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,991 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,991 INFO  L85        PathProgramCache]: Analyzing trace with hash -185959294, now seen corresponding path program 7 times
[2025-04-28 21:22:06,991 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,991 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [581239900]
[2025-04-28 21:22:06,991 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:06,991 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,998 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-04-28 21:22:07,012 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:22:07,012 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,012 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,520 INFO  L134       CoverageAnalysis]: Checked inductivity of 406 backedges. 0 proven. 210 refuted. 0 times theorem prover too weak. 196 trivial. 0 not checked.
[2025-04-28 21:22:07,521 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,521 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [581239900]
[2025-04-28 21:22:07,521 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [581239900] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,521 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1420780701]
[2025-04-28 21:22:07,521 INFO  L95    rtionOrderModulation]: Changing assertion order to NOT_INCREMENTALLY
[2025-04-28 21:22:07,521 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,523 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:07,525 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:07,528 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,633 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 65 statements into 1 equivalence classes.
[2025-04-28 21:22:07,667 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 65 of 65 statements.
[2025-04-28 21:22:07,667 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,667 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,673 INFO  L256         TraceCheckSpWp]: Trace formula consists of 192 conjuncts, 31 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,676 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:07,769 INFO  L134       CoverageAnalysis]: Checked inductivity of 406 backedges. 0 proven. 210 refuted. 0 times theorem prover too weak. 196 trivial. 0 not checked.
[2025-04-28 21:22:07,769 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
