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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:14,296 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:14,387 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b5d51e31-d46e-49d3-90f6-323d613404a4/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:14,399 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:14,399 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:14,435 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:14,436 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:14,436 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:14,436 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:14,436 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:14,437 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:14,437 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:14,437 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:14,437 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:14,437 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:14,437 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:14,438 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:14,438 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:14,438 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:14,438 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:14,438 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:14,438 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:14,438 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:14,439 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:14,439 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:14,439 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:14,440 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:14,769 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:14,780 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:14,783 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:14,786 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:14,786 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:14,788 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b5d51e31-d46e-49d3-90f6-323d613404a4/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-203.smt2
[2025-04-28 21:21:14,790 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:14,799 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:15,964 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b5d51e31-d46e-49d3-90f6-323d613404a4/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-203.smt2
[2025-04-28 21:21:15,967 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:15,971 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:15,972 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:15,972 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:15,972 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:15,975 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:16,066 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16 Unit
[2025-04-28 21:21:16,067 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:16,068 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:16,068 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:16,068 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:16,090 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,090 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,142 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,143 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,168 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,175 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,183 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,196 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,200 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,227 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:16,228 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:16,228 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:16,229 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:16,230 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (1/1) ...
[2025-04-28 21:21:16,233 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:16,252 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:16,268 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:16,274 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:16,288 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:16,289 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:16,289 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:16,289 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:16,289 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:16,289 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:16,290 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure step_lturn__bar given in one single declaration
[2025-04-28 21:21:16,290 INFO  L130     BoogieDeclarations]: Found specification of procedure step_lturn__bar
[2025-04-28 21:21:16,290 INFO  L138     BoogieDeclarations]: Found implementation of procedure step_lturn__bar
[2025-04-28 21:21:16,290 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure combined_lturn__bar given in one single declaration
[2025-04-28 21:21:16,290 INFO  L130     BoogieDeclarations]: Found specification of procedure combined_lturn__bar
[2025-04-28 21:21:16,290 INFO  L138     BoogieDeclarations]: Found implementation of procedure combined_lturn__bar
[2025-04-28 21:21:16,290 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure combined_lturn given in one single declaration
[2025-04-28 21:21:16,292 INFO  L130     BoogieDeclarations]: Found specification of procedure combined_lturn
[2025-04-28 21:21:16,292 INFO  L138     BoogieDeclarations]: Found implementation of procedure combined_lturn
[2025-04-28 21:21:16,292 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure lturn given in one single declaration
[2025-04-28 21:21:16,292 INFO  L130     BoogieDeclarations]: Found specification of procedure lturn
[2025-04-28 21:21:16,293 INFO  L138     BoogieDeclarations]: Found implementation of procedure lturn
[2025-04-28 21:21:16,293 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure step_lturn given in one single declaration
[2025-04-28 21:21:16,293 INFO  L130     BoogieDeclarations]: Found specification of procedure step_lturn
[2025-04-28 21:21:16,293 INFO  L138     BoogieDeclarations]: Found implementation of procedure step_lturn
[2025-04-28 21:21:16,293 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:16,293 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:16,293 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:16,393 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:16,396 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:17,432 INFO  L?                        ?]: Removed 8 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:17,432 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:17,454 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:17,457 INFO  L312             CfgBuilder]: Removed 37 assume(true) statements.
[2025-04-28 21:21:17,458 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17 BoogieIcfgContainer
[2025-04-28 21:21:17,458 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:17,464 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:17,464 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:17,468 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:17,472 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/3) ...
[2025-04-28 21:21:17,473 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@10fa89d0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,473 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:16" (2/3) ...
[2025-04-28 21:21:17,473 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@10fa89d0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:17, skipping insertion in model container
[2025-04-28 21:21:17,474 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:17" (3/3) ...
[2025-04-28 21:21:17,475 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:17,492 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:17,495 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 8 procedures, 123 locations, 427 edges, 8 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:17,547 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:17,571 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;@659735b6, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:17,571 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:17,578 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 123 states, 11 states have (on average 2.0) internal successors, (22), 12 states have internal predecessors, (22), 104 states have call successors, (135), 7 states have call predecessors, (135), 7 states have return successors, (135), 104 states have call predecessors, (135), 104 states have call successors, (135)
[2025-04-28 21:21:17,608 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:17,608 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,613 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:17,614 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,621 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,621 INFO  L85        PathProgramCache]: Analyzing trace with hash 362176697, now seen corresponding path program 1 times
[2025-04-28 21:21:17,629 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,630 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1826205142]
[2025-04-28 21:21:17,630 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,631 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,682 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:17,809 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:17,809 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,809 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,616 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:18,619 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,620 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1826205142]
[2025-04-28 21:21:18,620 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1826205142] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,621 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,625 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:18,628 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1757386180]
[2025-04-28 21:21:18,629 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,635 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:18,638 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,670 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:18,671 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:18,673 INFO  L87              Difference]: Start difference. First operand  has 123 states, 11 states have (on average 2.0) internal successors, (22), 12 states have internal predecessors, (22), 104 states have call successors, (135), 7 states have call predecessors, (135), 7 states have return successors, (135), 104 states have call predecessors, (135), 104 states have call successors, (135) 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:20,794 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,795 INFO  L93              Difference]: Finished difference Result 194 states and 589 transitions.
[2025-04-28 21:21:20,796 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:20,798 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:20,798 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,829 INFO  L225             Difference]: With dead ends: 194
[2025-04-28 21:21:20,829 INFO  L226             Difference]: Without dead ends: 193
[2025-04-28 21:21:20,833 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:20,840 INFO  L437           NwaCegarLoop]: 355 mSDtfsCounter, 1 mSDsluCounter, 1229 mSDsCounter, 0 mSdLazyCounter, 826 mSolverCounterSat, 62 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 73 SdHoareTripleChecker+Valid, 1584 SdHoareTripleChecker+Invalid, 888 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 62 IncrementalHoareTripleChecker+Valid, 826 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,843 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [73 Valid, 1584 Invalid, 888 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [62 Valid, 826 Invalid, 0 Unknown, 0 Unchecked, 1.9s Time]
[2025-04-28 21:21:20,869 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 193 states.
[2025-04-28 21:21:21,066 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 193 to 175.
[2025-04-28 21:21:21,072 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 175 states, 13 states have (on average 2.3846153846153846) internal successors, (31), 13 states have internal predecessors, (31), 154 states have call successors, (195), 9 states have call predecessors, (195), 9 states have return successors, (317), 154 states have call predecessors, (317), 154 states have call successors, (317)
[2025-04-28 21:21:21,085 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 175 states to 175 states and 543 transitions.
[2025-04-28 21:21:21,088 INFO  L79                 Accepts]: Start accepts. Automaton has 175 states and 543 transitions. Word has length 18
[2025-04-28 21:21:21,089 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,090 INFO  L485      AbstractCegarLoop]: Abstraction has 175 states and 543 transitions.
[2025-04-28 21:21:21,090 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:21,090 INFO  L278                IsEmpty]: Start isEmpty. Operand 175 states and 543 transitions.
[2025-04-28 21:21:21,103 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:21,105 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,105 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,105 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:21,106 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,107 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,107 INFO  L85        PathProgramCache]: Analyzing trace with hash -318554295, now seen corresponding path program 1 times
[2025-04-28 21:21:21,107 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,107 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1416768310]
[2025-04-28 21:21:21,107 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,108 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,126 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:21,166 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:21,167 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,167 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,649 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:21,650 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,650 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1416768310]
[2025-04-28 21:21:21,650 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1416768310] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,650 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,650 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:21,650 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1024615716]
[2025-04-28 21:21:21,650 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,652 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:21,652 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,652 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:21,653 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,654 INFO  L87              Difference]: Start difference. First operand 175 states and 543 transitions. Second operand  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:23,730 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,730 INFO  L93              Difference]: Finished difference Result 198 states and 638 transitions.
[2025-04-28 21:21:23,731 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:23,731 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 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:21:23,732 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,738 INFO  L225             Difference]: With dead ends: 198
[2025-04-28 21:21:23,738 INFO  L226             Difference]: Without dead ends: 198
[2025-04-28 21:21:23,738 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:23,739 INFO  L437           NwaCegarLoop]: 316 mSDtfsCounter, 1 mSDsluCounter, 1370 mSDsCounter, 0 mSdLazyCounter, 1235 mSolverCounterSat, 71 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 76 SdHoareTripleChecker+Valid, 1686 SdHoareTripleChecker+Invalid, 1306 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 71 IncrementalHoareTripleChecker+Valid, 1235 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,740 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [76 Valid, 1686 Invalid, 1306 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [71 Valid, 1235 Invalid, 0 Unknown, 0 Unchecked, 2.0s Time]
[2025-04-28 21:21:23,741 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 198 states.
[2025-04-28 21:21:23,830 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 198 to 188.
[2025-04-28 21:21:23,831 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 188 states, 14 states have (on average 2.2857142857142856) internal successors, (32), 14 states have internal predecessors, (32), 165 states have call successors, (206), 9 states have call predecessors, (206), 10 states have return successors, (374), 166 states have call predecessors, (374), 165 states have call successors, (374)
[2025-04-28 21:21:23,839 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 188 states to 188 states and 612 transitions.
[2025-04-28 21:21:23,839 INFO  L79                 Accepts]: Start accepts. Automaton has 188 states and 612 transitions. Word has length 21
[2025-04-28 21:21:23,840 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,840 INFO  L485      AbstractCegarLoop]: Abstraction has 188 states and 612 transitions.
[2025-04-28 21:21:23,840 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:23,840 INFO  L278                IsEmpty]: Start isEmpty. Operand 188 states and 612 transitions.
[2025-04-28 21:21:23,849 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:23,849 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,849 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, 1, 1, 1]
[2025-04-28 21:21:23,849 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:23,850 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,850 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,850 INFO  L85        PathProgramCache]: Analyzing trace with hash 663872231, now seen corresponding path program 1 times
[2025-04-28 21:21:23,850 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,850 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1919504342]
[2025-04-28 21:21:23,850 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,851 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,869 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:23,898 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:23,898 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,898 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,290 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:24,291 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,291 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1919504342]
[2025-04-28 21:21:24,291 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1919504342] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:24,291 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1759497321]
[2025-04-28 21:21:24,292 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,292 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:24,295 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:24,300 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:24,302 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:24,364 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:24,444 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:24,444 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,444 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,449 INFO  L256         TraceCheckSpWp]: Trace formula consists of 489 conjuncts, 24 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:24,458 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:24,789 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:24,789 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:26,989 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:26,989 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1759497321] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:26,989 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:26,989 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 17
[2025-04-28 21:21:26,989 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [448796444]
[2025-04-28 21:21:26,990 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,991 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 17 states
[2025-04-28 21:21:26,992 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,993 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 17 interpolants.
[2025-04-28 21:21:26,993 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=235, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:26,994 INFO  L87              Difference]: Start difference. First operand 188 states and 612 transitions. Second operand  has 17 states, 14 states have (on average 1.4285714285714286) internal successors, (20), 13 states have internal predecessors, (20), 4 states have call successors, (9), 1 states have call predecessors, (9), 13 states have return successors, (15), 11 states have call predecessors, (15), 4 states have call successors, (15)
[2025-04-28 21:21:33,757 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,758 INFO  L93              Difference]: Finished difference Result 467 states and 3092 transitions.
[2025-04-28 21:21:33,758 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:33,758 INFO  L79                 Accepts]: Start accepts. Automaton has  has 17 states, 14 states have (on average 1.4285714285714286) internal successors, (20), 13 states have internal predecessors, (20), 4 states have call successors, (9), 1 states have call predecessors, (9), 13 states have return successors, (15), 11 states have call predecessors, (15), 4 states have call successors, (15) Word has length 24
[2025-04-28 21:21:33,759 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,783 INFO  L225             Difference]: With dead ends: 467
[2025-04-28 21:21:33,783 INFO  L226             Difference]: Without dead ends: 467
[2025-04-28 21:21:33,784 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 40 SyntacticMatches, 0 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=49, Invalid=331, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:33,787 INFO  L437           NwaCegarLoop]: 271 mSDtfsCounter, 2 mSDsluCounter, 3134 mSDsCounter, 0 mSdLazyCounter, 5364 mSolverCounterSat, 286 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 5.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 242 SdHoareTripleChecker+Valid, 3405 SdHoareTripleChecker+Invalid, 5650 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 286 IncrementalHoareTripleChecker+Valid, 5364 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 6.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,787 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [242 Valid, 3405 Invalid, 5650 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [286 Valid, 5364 Invalid, 0 Unknown, 0 Unchecked, 6.4s Time]
[2025-04-28 21:21:33,789 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 467 states.
[2025-04-28 21:21:34,396 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 467 to 287.
[2025-04-28 21:21:34,400 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 287 states, 23 states have (on average 2.5652173913043477) internal successors, (59), 21 states have internal predecessors, (59), 250 states have call successors, (311), 13 states have call predecessors, (311), 17 states have return successors, (1166), 254 states have call predecessors, (1166), 250 states have call successors, (1166)
[2025-04-28 21:21:34,409 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 287 states to 287 states and 1536 transitions.
[2025-04-28 21:21:34,409 INFO  L79                 Accepts]: Start accepts. Automaton has 287 states and 1536 transitions. Word has length 24
[2025-04-28 21:21:34,409 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,409 INFO  L485      AbstractCegarLoop]: Abstraction has 287 states and 1536 transitions.
[2025-04-28 21:21:34,410 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 17 states, 14 states have (on average 1.4285714285714286) internal successors, (20), 13 states have internal predecessors, (20), 4 states have call successors, (9), 1 states have call predecessors, (9), 13 states have return successors, (15), 11 states have call predecessors, (15), 4 states have call successors, (15)
[2025-04-28 21:21:34,410 INFO  L278                IsEmpty]: Start isEmpty. Operand 287 states and 1536 transitions.
[2025-04-28 21:21:34,423 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:34,423 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,424 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,430 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:34,628 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:34,628 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,629 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,629 INFO  L85        PathProgramCache]: Analyzing trace with hash 1675590411, now seen corresponding path program 1 times
[2025-04-28 21:21:34,629 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,629 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1770915377]
[2025-04-28 21:21:34,629 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,629 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,645 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:34,668 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:34,673 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,673 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,008 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:35,008 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,008 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1770915377]
[2025-04-28 21:21:35,008 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1770915377] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,008 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:35,008 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:35,008 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [378409878]
[2025-04-28 21:21:35,008 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,009 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:35,009 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,009 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:35,009 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:35,010 INFO  L87              Difference]: Start difference. First operand 287 states and 1536 transitions. Second operand  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:36,653 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,654 INFO  L93              Difference]: Finished difference Result 514 states and 3897 transitions.
[2025-04-28 21:21:36,654 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:36,655 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 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:21:36,655 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,680 INFO  L225             Difference]: With dead ends: 514
[2025-04-28 21:21:36,680 INFO  L226             Difference]: Without dead ends: 513
[2025-04-28 21:21:36,680 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:36,681 INFO  L437           NwaCegarLoop]: 340 mSDtfsCounter, 9 mSDsluCounter, 1490 mSDsCounter, 0 mSdLazyCounter, 1145 mSolverCounterSat, 66 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 92 SdHoareTripleChecker+Valid, 1830 SdHoareTripleChecker+Invalid, 1211 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 66 IncrementalHoareTripleChecker+Valid, 1145 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,682 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [92 Valid, 1830 Invalid, 1211 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [66 Valid, 1145 Invalid, 0 Unknown, 0 Unchecked, 1.6s Time]
[2025-04-28 21:21:36,686 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 513 states.
[2025-04-28 21:21:37,405 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 513 to 480.
[2025-04-28 21:21:37,409 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 480 states, 37 states have (on average 2.5675675675675675) internal successors, (95), 34 states have internal predecessors, (95), 421 states have call successors, (509), 19 states have call predecessors, (509), 28 states have return successors, (3060), 430 states have call predecessors, (3060), 421 states have call successors, (3060)
[2025-04-28 21:21:37,437 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 480 states to 480 states and 3664 transitions.
[2025-04-28 21:21:37,438 INFO  L79                 Accepts]: Start accepts. Automaton has 480 states and 3664 transitions. Word has length 21
[2025-04-28 21:21:37,438 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,438 INFO  L485      AbstractCegarLoop]: Abstraction has 480 states and 3664 transitions.
[2025-04-28 21:21:37,438 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:37,438 INFO  L278                IsEmpty]: Start isEmpty. Operand 480 states and 3664 transitions.
[2025-04-28 21:21:37,461 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:37,461 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,461 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:37,461 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:37,461 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,463 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,463 INFO  L85        PathProgramCache]: Analyzing trace with hash -1910556099, now seen corresponding path program 1 times
[2025-04-28 21:21:37,463 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,464 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [9254600]
[2025-04-28 21:21:37,464 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,464 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,479 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:37,502 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:37,502 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,502 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,915 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:37,916 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,916 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [9254600]
[2025-04-28 21:21:37,916 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [9254600] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,916 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:37,916 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:37,916 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2074535193]
[2025-04-28 21:21:37,916 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,917 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:37,917 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,917 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:37,917 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:37,918 INFO  L87              Difference]: Start difference. First operand 480 states and 3664 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:39,125 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,125 INFO  L93              Difference]: Finished difference Result 736 states and 7387 transitions.
[2025-04-28 21:21:39,126 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:39,126 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:39,126 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,173 INFO  L225             Difference]: With dead ends: 736
[2025-04-28 21:21:39,173 INFO  L226             Difference]: Without dead ends: 735
[2025-04-28 21:21:39,173 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:39,174 INFO  L437           NwaCegarLoop]: 333 mSDtfsCounter, 1 mSDsluCounter, 1175 mSDsCounter, 0 mSdLazyCounter, 700 mSolverCounterSat, 14 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 50 SdHoareTripleChecker+Valid, 1508 SdHoareTripleChecker+Invalid, 714 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 14 IncrementalHoareTripleChecker+Valid, 700 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,174 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [50 Valid, 1508 Invalid, 714 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [14 Valid, 700 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:21:39,175 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 735 states.
[2025-04-28 21:21:40,811 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 735 to 608.
[2025-04-28 21:21:40,817 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 608 states, 53 states have (on average 2.0943396226415096) internal successors, (111), 50 states have internal predecessors, (111), 517 states have call successors, (605), 19 states have call predecessors, (605), 44 states have return successors, (5521), 542 states have call predecessors, (5521), 517 states have call successors, (5521)
[2025-04-28 21:21:40,853 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 608 states to 608 states and 6237 transitions.
[2025-04-28 21:21:40,853 INFO  L79                 Accepts]: Start accepts. Automaton has 608 states and 6237 transitions. Word has length 18
[2025-04-28 21:21:40,853 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,854 INFO  L485      AbstractCegarLoop]: Abstraction has 608 states and 6237 transitions.
[2025-04-28 21:21:40,854 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:40,854 INFO  L278                IsEmpty]: Start isEmpty. Operand 608 states and 6237 transitions.
[2025-04-28 21:21:40,872 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:40,872 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,872 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,872 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:40,873 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,874 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,875 INFO  L85        PathProgramCache]: Analyzing trace with hash -1436825787, now seen corresponding path program 1 times
[2025-04-28 21:21:40,875 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,875 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [575211947]
[2025-04-28 21:21:40,875 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,875 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,887 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:40,904 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:40,905 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,905 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,363 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:41,363 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,363 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [575211947]
[2025-04-28 21:21:41,363 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [575211947] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,364 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,364 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:41,364 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1041214571]
[2025-04-28 21:21:41,364 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,364 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:41,364 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,364 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:41,365 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:41,365 INFO  L87              Difference]: Start difference. First operand 608 states and 6237 transitions. Second operand  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:42,971 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,971 INFO  L93              Difference]: Finished difference Result 735 states and 7382 transitions.
[2025-04-28 21:21:42,972 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:42,972 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 6 states have (on average 1.5) internal successors, (9), 5 states have internal predecessors, (9), 2 states have call successors, (6), 1 states have call predecessors, (6), 5 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:21:42,972 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,005 INFO  L225             Difference]: With dead ends: 735
[2025-04-28 21:21:43,005 INFO  L226             Difference]: Without dead ends: 735
[2025-04-28 21:21:43,005 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:43,007 INFO  L437           NwaCegarLoop]: 324 mSDtfsCounter, 1 mSDsluCounter, 1427 mSDsCounter, 0 mSdLazyCounter, 1062 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 50 SdHoareTripleChecker+Valid, 1751 SdHoareTripleChecker+Invalid, 1075 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 1062 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,009 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [50 Valid, 1751 Invalid, 1075 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 1062 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-04-28 21:21:43,010 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 735 states.
