./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-206.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:39,187 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:39,275 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_76939ff3-6a9e-4e2d-9b53-ab868fb3970a/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:39,287 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:39,287 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:39,310 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:39,310 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:39,310 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:39,311 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:39,311 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:39,311 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:39,311 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:39,311 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:39,311 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:39,311 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:39,312 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:39,312 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:39,312 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:39,314 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:39,314 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:39,314 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:39,314 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:39,315 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:39,315 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:39,315 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:39,316 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:39,316 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:39,654 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:39,668 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:39,670 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:39,673 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:39,673 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:39,676 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_76939ff3-6a9e-4e2d-9b53-ab868fb3970a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-206.smt2
[2025-04-28 21:21:39,680 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:39,684 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:40,306 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_76939ff3-6a9e-4e2d-9b53-ab868fb3970a/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-206.smt2
[2025-04-28 21:21:40,311 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:40,312 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:40,315 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:40,315 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:40,315 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:40,322 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,394 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40 Unit
[2025-04-28 21:21:40,394 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:40,396 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:40,397 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:40,397 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:40,413 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,413 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,439 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,439 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,449 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,452 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,455 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,459 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,461 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,493 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:40,493 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:40,494 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:40,494 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:40,495 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (1/1) ...
[2025-04-28 21:21:40,497 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,512 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,527 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:40,531 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:40,547 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:40,547 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:40,547 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:40,547 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:40,547 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:40,547 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:40,548 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure step_lturn given in one single declaration
[2025-04-28 21:21:40,548 INFO  L130     BoogieDeclarations]: Found specification of procedure step_lturn
[2025-04-28 21:21:40,548 INFO  L138     BoogieDeclarations]: Found implementation of procedure step_lturn
[2025-04-28 21:21:40,548 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure combined_lturn given in one single declaration
[2025-04-28 21:21:40,548 INFO  L130     BoogieDeclarations]: Found specification of procedure combined_lturn
[2025-04-28 21:21:40,549 INFO  L138     BoogieDeclarations]: Found implementation of procedure combined_lturn
[2025-04-28 21:21:40,549 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure lturn given in one single declaration
[2025-04-28 21:21:40,549 INFO  L130     BoogieDeclarations]: Found specification of procedure lturn
[2025-04-28 21:21:40,549 INFO  L138     BoogieDeclarations]: Found implementation of procedure lturn
[2025-04-28 21:21:40,551 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:40,551 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:40,551 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:40,625 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:40,627 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:41,391 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:41,392 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:41,414 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:41,418 INFO  L312             CfgBuilder]: Removed 17 assume(true) statements.
[2025-04-28 21:21:41,422 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41 BoogieIcfgContainer
[2025-04-28 21:21:41,422 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:41,425 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:41,427 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:41,432 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:41,432 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:40" (1/3) ...
[2025-04-28 21:21:41,433 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1d9d08b3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,433 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:40" (2/3) ...
[2025-04-28 21:21:41,433 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@1d9d08b3 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:41, skipping insertion in model container
[2025-04-28 21:21:41,433 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:41" (3/3) ...
[2025-04-28 21:21:41,435 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:41,452 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:41,454 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 6 procedures, 132 locations, 421 edges, 6 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:41,499 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:41,512 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;@61b20fa, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:41,512 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:41,516 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 132 states, 10 states have (on average 3.1) internal successors, (31), 26 states have internal predecessors, (31), 118 states have call successors, (130), 5 states have call predecessors, (130), 5 states have return successors, (130), 102 states have call predecessors, (130), 118 states have call successors, (130)
[2025-04-28 21:21:41,548 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:41,548 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,552 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,553 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,559 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,559 INFO  L85        PathProgramCache]: Analyzing trace with hash -561249361, now seen corresponding path program 1 times
[2025-04-28 21:21:41,567 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,568 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2050649251]
[2025-04-28 21:21:41,568 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,569 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,612 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:41,735 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:41,735 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,735 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,717 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:42,717 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,717 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2050649251]
[2025-04-28 21:21:42,718 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2050649251] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,718 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,724 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:42,726 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [841378635]
[2025-04-28 21:21:42,727 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,732 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:42,735 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,799 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:42,800 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,803 INFO  L87              Difference]: Start difference. First operand  has 132 states, 10 states have (on average 3.1) internal successors, (31), 26 states have internal predecessors, (31), 118 states have call successors, (130), 5 states have call predecessors, (130), 5 states have return successors, (130), 102 states have call predecessors, (130), 118 states have call successors, (130) Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:44,826 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,827 INFO  L93              Difference]: Finished difference Result 184 states and 564 transitions.
[2025-04-28 21:21:44,828 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:44,830 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 18
[2025-04-28 21:21:44,830 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,848 INFO  L225             Difference]: With dead ends: 184
[2025-04-28 21:21:44,848 INFO  L226             Difference]: Without dead ends: 184
[2025-04-28 21:21:44,850 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:44,856 INFO  L437           NwaCegarLoop]: 262 mSDtfsCounter, 8 mSDsluCounter, 869 mSDsCounter, 0 mSdLazyCounter, 929 mSolverCounterSat, 36 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 77 SdHoareTripleChecker+Valid, 1131 SdHoareTripleChecker+Invalid, 965 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 36 IncrementalHoareTripleChecker+Valid, 929 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,857 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [77 Valid, 1131 Invalid, 965 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [36 Valid, 929 Invalid, 0 Unknown, 0 Unchecked, 1.9s Time]
[2025-04-28 21:21:44,874 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 184 states.
[2025-04-28 21:21:45,094 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 184 to 181.
[2025-04-28 21:21:45,096 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 181 states, 13 states have (on average 3.3076923076923075) internal successors, (43), 33 states have internal predecessors, (43), 163 states have call successors, (179), 7 states have call predecessors, (179), 8 states have return successors, (337), 143 states have call predecessors, (337), 163 states have call successors, (337)
[2025-04-28 21:21:45,109 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 181 states to 181 states and 559 transitions.
[2025-04-28 21:21:45,110 INFO  L79                 Accepts]: Start accepts. Automaton has 181 states and 559 transitions. Word has length 18
[2025-04-28 21:21:45,112 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,112 INFO  L485      AbstractCegarLoop]: Abstraction has 181 states and 559 transitions.
[2025-04-28 21:21:45,112 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:45,112 INFO  L278                IsEmpty]: Start isEmpty. Operand 181 states and 559 transitions.
[2025-04-28 21:21:45,125 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:45,125 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,125 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,126 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:45,126 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,127 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,128 INFO  L85        PathProgramCache]: Analyzing trace with hash 253134473, now seen corresponding path program 1 times
[2025-04-28 21:21:45,128 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,129 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1322519351]
[2025-04-28 21:21:45,129 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,129 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,144 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:45,172 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:45,177 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,177 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,403 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:45,403 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,403 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1322519351]
[2025-04-28 21:21:45,403 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1322519351] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,404 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,404 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:45,404 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [332553262]
[2025-04-28 21:21:45,404 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,405 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:45,405 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,406 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:45,406 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:45,406 INFO  L87              Difference]: Start difference. First operand 181 states and 559 transitions. Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:46,866 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,867 INFO  L93              Difference]: Finished difference Result 278 states and 1209 transitions.
[2025-04-28 21:21:46,867 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:46,867 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 18
[2025-04-28 21:21:46,868 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,882 INFO  L225             Difference]: With dead ends: 278
[2025-04-28 21:21:46,882 INFO  L226             Difference]: Without dead ends: 278
[2025-04-28 21:21:46,882 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:46,883 INFO  L437           NwaCegarLoop]: 319 mSDtfsCounter, 6 mSDsluCounter, 1077 mSDsCounter, 0 mSdLazyCounter, 919 mSolverCounterSat, 46 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 61 SdHoareTripleChecker+Valid, 1396 SdHoareTripleChecker+Invalid, 965 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 46 IncrementalHoareTripleChecker+Valid, 919 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,883 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [61 Valid, 1396 Invalid, 965 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [46 Valid, 919 Invalid, 0 Unknown, 0 Unchecked, 1.4s Time]
[2025-04-28 21:21:46,885 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 278 states.
[2025-04-28 21:21:47,142 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 278 to 276.
[2025-04-28 21:21:47,143 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 276 states, 20 states have (on average 3.1) internal successors, (62), 49 states have internal predecessors, (62), 248 states have call successors, (272), 11 states have call predecessors, (272), 13 states have return successors, (873), 219 states have call predecessors, (873), 248 states have call successors, (873)
[2025-04-28 21:21:47,154 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 276 states to 276 states and 1207 transitions.
[2025-04-28 21:21:47,154 INFO  L79                 Accepts]: Start accepts. Automaton has 276 states and 1207 transitions. Word has length 18
[2025-04-28 21:21:47,155 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,155 INFO  L485      AbstractCegarLoop]: Abstraction has 276 states and 1207 transitions.
[2025-04-28 21:21:47,155 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:47,155 INFO  L278                IsEmpty]: Start isEmpty. Operand 276 states and 1207 transitions.
[2025-04-28 21:21:47,163 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:47,163 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,163 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,164 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:47,164 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,165 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,165 INFO  L85        PathProgramCache]: Analyzing trace with hash 1122998981, now seen corresponding path program 1 times
[2025-04-28 21:21:47,165 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,165 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1778546170]
[2025-04-28 21:21:47,165 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,165 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,179 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:47,196 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:47,196 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,198 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,397 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:47,397 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,397 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1778546170]
[2025-04-28 21:21:47,397 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1778546170] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,397 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1930427287]
[2025-04-28 21:21:47,397 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,398 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,400 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,405 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:47,409 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,462 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:47,520 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:47,520 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,521 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,528 INFO  L256         TraceCheckSpWp]: Trace formula consists of 303 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,535 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,663 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:47,663 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,102 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:48,102 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1930427287] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,102 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,102 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:48,102 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1174554062]
[2025-04-28 21:21:48,102 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,103 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:48,103 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,103 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:48,103 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:48,104 INFO  L87              Difference]: Start difference. First operand 276 states and 1207 transitions. Second operand  has 10 states, 8 states have (on average 1.625) internal successors, (13), 7 states have internal predecessors, (13), 3 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:51,228 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,228 INFO  L93              Difference]: Finished difference Result 381 states and 2299 transitions.
[2025-04-28 21:21:51,228 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:51,229 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 1.625) internal successors, (13), 7 states have internal predecessors, (13), 3 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8) Word has length 18
[2025-04-28 21:21:51,229 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,255 INFO  L225             Difference]: With dead ends: 381
[2025-04-28 21:21:51,255 INFO  L226             Difference]: Without dead ends: 381
[2025-04-28 21:21:51,256 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 48 GetRequests, 30 SyntacticMatches, 4 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 13 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=49, Invalid=191, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:51,257 INFO  L437           NwaCegarLoop]: 314 mSDtfsCounter, 13 mSDsluCounter, 1947 mSDsCounter, 0 mSdLazyCounter, 2416 mSolverCounterSat, 283 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 78 SdHoareTripleChecker+Valid, 2261 SdHoareTripleChecker+Invalid, 2699 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 283 IncrementalHoareTripleChecker+Valid, 2416 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,257 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [78 Valid, 2261 Invalid, 2699 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [283 Valid, 2416 Invalid, 0 Unknown, 0 Unchecked, 2.9s Time]
[2025-04-28 21:21:51,258 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 381 states.
[2025-04-28 21:21:51,677 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 381 to 376.
[2025-04-28 21:21:51,681 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 376 states, 33 states have (on average 2.5757575757575757) internal successors, (85), 70 states have internal predecessors, (85), 326 states have call successors, (358), 15 states have call predecessors, (358), 24 states have return successors, (1848), 294 states have call predecessors, (1848), 326 states have call successors, (1848)
[2025-04-28 21:21:51,696 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 376 states to 376 states and 2291 transitions.
[2025-04-28 21:21:51,697 INFO  L79                 Accepts]: Start accepts. Automaton has 376 states and 2291 transitions. Word has length 18
[2025-04-28 21:21:51,698 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,701 INFO  L485      AbstractCegarLoop]: Abstraction has 376 states and 2291 transitions.
[2025-04-28 21:21:51,701 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 1.625) internal successors, (13), 7 states have internal predecessors, (13), 3 states have call successors, (6), 1 states have call predecessors, (6), 7 states have return successors, (8), 5 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:51,701 INFO  L278                IsEmpty]: Start isEmpty. Operand 376 states and 2291 transitions.
[2025-04-28 21:21:51,713 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:51,713 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,713 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,720 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:51,916 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,916 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,917 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,917 INFO  L85        PathProgramCache]: Analyzing trace with hash 786383523, now seen corresponding path program 1 times
[2025-04-28 21:21:51,918 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,918 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1123977092]
[2025-04-28 21:21:51,918 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:51,918 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,927 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:51,938 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:51,938 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:51,938 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,171 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:52,171 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,171 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1123977092]
[2025-04-28 21:21:52,171 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1123977092] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,171 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2043013955]
[2025-04-28 21:21:52,171 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,172 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,174 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,177 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:52,182 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,230 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:52,281 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:52,281 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,281 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,283 INFO  L256         TraceCheckSpWp]: Trace formula consists of 329 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,286 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,370 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:52,372 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,004 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:53,004 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2043013955] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,005 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,005 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:53,005 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [75222628]
[2025-04-28 21:21:53,006 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,006 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:53,006 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,007 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:53,007 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=17, Invalid=73, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:53,007 INFO  L87              Difference]: Start difference. First operand 376 states and 2291 transitions. Second operand  has 10 states, 8 states have (on average 1.625) internal successors, (13), 7 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 7 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:56,046 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,046 INFO  L93              Difference]: Finished difference Result 524 states and 4319 transitions.
[2025-04-28 21:21:56,046 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:56,047 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 8 states have (on average 1.625) internal successors, (13), 7 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 7 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10) Word has length 21
[2025-04-28 21:21:56,047 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,092 INFO  L225             Difference]: With dead ends: 524
[2025-04-28 21:21:56,092 INFO  L226             Difference]: Without dead ends: 524
[2025-04-28 21:21:56,093 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 55 GetRequests, 36 SyntacticMatches, 5 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 13 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=49, Invalid=191, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:56,093 INFO  L437           NwaCegarLoop]: 295 mSDtfsCounter, 13 mSDsluCounter, 1798 mSDsCounter, 0 mSdLazyCounter, 2372 mSolverCounterSat, 283 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 82 SdHoareTripleChecker+Valid, 2093 SdHoareTripleChecker+Invalid, 2655 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 283 IncrementalHoareTripleChecker+Valid, 2372 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,094 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [82 Valid, 2093 Invalid, 2655 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [283 Valid, 2372 Invalid, 0 Unknown, 0 Unchecked, 2.8s Time]
[2025-04-28 21:21:56,095 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 524 states.
[2025-04-28 21:21:56,722 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 524 to 519.
[2025-04-28 21:21:56,726 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 519 states, 52 states have (on average 2.2884615384615383) internal successors, (119), 101 states have internal predecessors, (119), 437 states have call successors, (481), 21 states have call predecessors, (481), 40 states have return successors, (3710), 400 states have call predecessors, (3710), 437 states have call successors, (3710)
[2025-04-28 21:21:56,758 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 519 states to 519 states and 4310 transitions.
[2025-04-28 21:21:56,758 INFO  L79                 Accepts]: Start accepts. Automaton has 519 states and 4310 transitions. Word has length 21
[2025-04-28 21:21:56,759 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,759 INFO  L485      AbstractCegarLoop]: Abstraction has 519 states and 4310 transitions.
[2025-04-28 21:21:56,759 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 8 states have (on average 1.625) internal successors, (13), 7 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 7 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:56,759 INFO  L278                IsEmpty]: Start isEmpty. Operand 519 states and 4310 transitions.
[2025-04-28 21:21:56,778 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:56,778 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,778 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,784 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:56,983 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,983 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,983 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,984 INFO  L85        PathProgramCache]: Analyzing trace with hash -347917193, now seen corresponding path program 1 times
[2025-04-28 21:21:56,984 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,984 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1101306668]
[2025-04-28 21:21:56,984 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,984 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,992 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:57,008 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:57,008 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,008 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,232 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:57,232 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,232 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1101306668]
[2025-04-28 21:21:57,232 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1101306668] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,232 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [421840572]
[2025-04-28 21:21:57,232 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,232 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,236 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,238 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:57,241 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,292 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:57,337 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:57,337 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,337 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,339 INFO  L256         TraceCheckSpWp]: Trace formula consists of 329 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,341 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,439 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:57,440 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,051 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:58,051 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [421840572] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:58,051 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:58,052 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [7, 7, 7] total 12
[2025-04-28 21:21:58,052 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1863607479]
[2025-04-28 21:21:58,052 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,052 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:58,052 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,053 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:58,053 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=21, Invalid=111, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:58,053 INFO  L87              Difference]: Start difference. First operand 519 states and 4310 transitions. Second operand  has 12 states, 10 states have (on average 1.5) internal successors, (15), 9 states have internal predecessors, (15), 3 states have call successors, (7), 1 states have call predecessors, (7), 9 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:22:02,343 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,343 INFO  L93              Difference]: Finished difference Result 1051 states and 15866 transitions.
[2025-04-28 21:22:02,343 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:22:02,344 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 10 states have (on average 1.5) internal successors, (15), 9 states have internal predecessors, (15), 3 states have call successors, (7), 1 states have call predecessors, (7), 9 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10) Word has length 21
[2025-04-28 21:22:02,344 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,527 INFO  L225             Difference]: With dead ends: 1051
[2025-04-28 21:22:02,528 INFO  L226             Difference]: Without dead ends: 1051
[2025-04-28 21:22:02,528 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 57 GetRequests, 35 SyntacticMatches, 5 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 19 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=57, Invalid=285, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:22:02,529 INFO  L437           NwaCegarLoop]: 316 mSDtfsCounter, 23 mSDsluCounter, 2462 mSDsCounter, 0 mSdLazyCounter, 3643 mSolverCounterSat, 457 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 3.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 132 SdHoareTripleChecker+Valid, 2778 SdHoareTripleChecker+Invalid, 4100 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 457 IncrementalHoareTripleChecker+Valid, 3643 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 3.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,529 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [132 Valid, 2778 Invalid, 4100 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [457 Valid, 3643 Invalid, 0 Unknown, 0 Unchecked, 3.9s Time]
[2025-04-28 21:22:02,530 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1051 states.
[2025-04-28 21:22:05,369 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1051 to 1046.
[2025-04-28 21:22:05,383 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1046 states, 103 states have (on average 2.29126213592233) internal successors, (236), 204 states have internal predecessors, (236), 888 states have call successors, (982), 45 states have call predecessors, (982), 78 states have return successors, (14637), 800 states have call predecessors, (14637), 888 states have call successors, (14637)
[2025-04-28 21:22:05,543 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1046 states to 1046 states and 15855 transitions.
[2025-04-28 21:22:05,545 INFO  L79                 Accepts]: Start accepts. Automaton has 1046 states and 15855 transitions. Word has length 21
[2025-04-28 21:22:05,545 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:05,546 INFO  L485      AbstractCegarLoop]: Abstraction has 1046 states and 15855 transitions.
[2025-04-28 21:22:05,546 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 10 states have (on average 1.5) internal successors, (15), 9 states have internal predecessors, (15), 3 states have call successors, (7), 1 states have call predecessors, (7), 9 states have return successors, (10), 7 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:22:05,546 INFO  L278                IsEmpty]: Start isEmpty. Operand 1046 states and 15855 transitions.
[2025-04-28 21:22:05,578 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:22:05,578 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:05,578 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:05,584 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:22:05,782 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:05,782 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:05,784 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:05,785 INFO  L85        PathProgramCache]: Analyzing trace with hash -131757343, now seen corresponding path program 1 times
[2025-04-28 21:22:05,785 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:05,785 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [307736358]
[2025-04-28 21:22:05,785 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:05,785 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:05,793 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:22:05,813 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:05,813 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:05,813 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:06,323 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:22:06,323 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:06,324 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [307736358]
[2025-04-28 21:22:06,325 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [307736358] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:06,325 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:06,325 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:06,325 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1887764173]
[2025-04-28 21:22:06,325 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:06,325 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:06,326 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:06,326 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:06,327 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:06,328 INFO  L87              Difference]: Start difference. First operand 1046 states and 15855 transitions. Second operand  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:22:07,791 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:07,792 INFO  L93              Difference]: Finished difference Result 1119 states and 18048 transitions.
[2025-04-28 21:22:07,792 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:07,793 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.6) internal successors, (8), 4 states have internal predecessors, (8), 2 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6) Word has length 21
[2025-04-28 21:22:07,793 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:08,053 INFO  L225             Difference]: With dead ends: 1119
[2025-04-28 21:22:08,053 INFO  L226             Difference]: Without dead ends: 1119
[2025-04-28 21:22:08,053 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:08,054 INFO  L437           NwaCegarLoop]: 294 mSDtfsCounter, 8 mSDsluCounter, 989 mSDsCounter, 0 mSdLazyCounter, 930 mSolverCounterSat, 36 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 56 SdHoareTripleChecker+Valid, 1283 SdHoareTripleChecker+Invalid, 966 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 36 IncrementalHoareTripleChecker+Valid, 930 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:08,054 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [56 Valid, 1283 Invalid, 966 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [36 Valid, 930 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-04-28 21:22:08,056 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1119 states.
[2025-04-28 21:22:10,561 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1119 to 1115.
[2025-04-28 21:22:10,572 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1115 states, 109 states have (on average 2.220183486238532) internal successors, (242), 210 states have internal predecessors, (242), 945 states have call successors, (1039), 45 states have call predecessors, (1039), 84 states have return successors, (16737), 863 states have call predecessors, (16737), 945 states have call successors, (16737)
