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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:34,299 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:34,395 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5a955303-823c-4c74-9848-3087087bc3f1/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:34,404 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:34,404 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:34,436 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:34,438 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:34,438 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:34,440 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:34,440 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:34,440 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:34,441 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:34,441 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:34,441 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:34,441 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:34,441 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:34,441 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:34,441 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:34,441 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:34,441 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:34,442 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:34,442 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:34,442 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:34,442 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:34,443 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:34,444 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:34,444 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:34,777 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:34,788 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:34,792 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:34,794 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:34,794 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:34,795 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5a955303-823c-4c74-9848-3087087bc3f1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-185.smt2
[2025-04-28 21:21:34,800 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:34,803 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:35,384 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5a955303-823c-4c74-9848-3087087bc3f1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-185.smt2
[2025-04-28 21:21:35,388 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:35,391 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:35,393 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:35,393 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:35,393 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:35,396 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,474 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35 Unit
[2025-04-28 21:21:35,480 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:35,481 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:35,481 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:35,482 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:35,503 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,504 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,542 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,543 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,556 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,558 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,561 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,565 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,567 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,587 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:35,588 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:35,588 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:35,588 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:35,589 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,593 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:35,608 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,624 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:35,627 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:35,646 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:35,647 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:35,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:35,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:35,647 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:35,647 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:35,647 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure step_lturn given in one single declaration
[2025-04-28 21:21:35,647 INFO  L130     BoogieDeclarations]: Found specification of procedure step_lturn
[2025-04-28 21:21:35,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure step_lturn
[2025-04-28 21:21:35,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure combined_lturn given in one single declaration
[2025-04-28 21:21:35,648 INFO  L130     BoogieDeclarations]: Found specification of procedure combined_lturn
[2025-04-28 21:21:35,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure combined_lturn
[2025-04-28 21:21:35,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure lturn given in one single declaration
[2025-04-28 21:21:35,648 INFO  L130     BoogieDeclarations]: Found specification of procedure lturn
[2025-04-28 21:21:35,648 INFO  L138     BoogieDeclarations]: Found implementation of procedure lturn
[2025-04-28 21:21:35,648 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:35,648 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:35,649 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:35,722 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:35,727 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:36,558 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:36,560 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:36,587 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:36,591 INFO  L312             CfgBuilder]: Removed 17 assume(true) statements.
[2025-04-28 21:21:36,592 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:36 BoogieIcfgContainer
[2025-04-28 21:21:36,592 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:36,599 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:36,599 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:36,603 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:36,605 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:35" (1/3) ...
[2025-04-28 21:21:36,606 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5fda4856 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:36, skipping insertion in model container
[2025-04-28 21:21:36,607 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (2/3) ...
[2025-04-28 21:21:36,607 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@5fda4856 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:36, skipping insertion in model container
[2025-04-28 21:21:36,607 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:36" (3/3) ...
[2025-04-28 21:21:36,611 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:36,624 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:36,626 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:36,676 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:36,689 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;@5d80f2f9, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:36,689 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:36,693 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:36,721 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:36,722 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,723 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:36,723 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,728 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,729 INFO  L85        PathProgramCache]: Analyzing trace with hash 243736157, now seen corresponding path program 1 times
[2025-04-28 21:21:36,737 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,738 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1319658308]
[2025-04-28 21:21:36,738 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,739 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,786 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:36,921 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:36,925 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,925 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,554 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,555 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,555 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1319658308]
[2025-04-28 21:21:37,555 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1319658308] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,556 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:37,595 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:37,597 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [552756743]
[2025-04-28 21:21:37,598 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,605 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:37,605 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,643 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:37,643 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:37,646 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:39,967 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,968 INFO  L93              Difference]: Finished difference Result 217 states and 663 transitions.
[2025-04-28 21:21:39,970 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:39,972 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,972 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,011 INFO  L225             Difference]: With dead ends: 217
[2025-04-28 21:21:40,012 INFO  L226             Difference]: Without dead ends: 217
[2025-04-28 21:21:40,018 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:40,022 INFO  L437           NwaCegarLoop]: 267 mSDtfsCounter, 11 mSDsluCounter, 862 mSDsCounter, 0 mSdLazyCounter, 1023 mSolverCounterSat, 68 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 116 SdHoareTripleChecker+Valid, 1129 SdHoareTripleChecker+Invalid, 1091 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 68 IncrementalHoareTripleChecker+Valid, 1023 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,023 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [116 Valid, 1129 Invalid, 1091 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [68 Valid, 1023 Invalid, 0 Unknown, 0 Unchecked, 2.1s Time]
[2025-04-28 21:21:40,043 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 217 states.
[2025-04-28 21:21:40,260 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 217 to 208.
[2025-04-28 21:21:40,264 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 208 states, 14 states have (on average 3.2142857142857144) internal successors, (45), 38 states have internal predecessors, (45), 190 states have call successors, (209), 8 states have call predecessors, (209), 8 states have return successors, (386), 164 states have call predecessors, (386), 190 states have call successors, (386)
[2025-04-28 21:21:40,281 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 208 states to 208 states and 640 transitions.
[2025-04-28 21:21:40,283 INFO  L79                 Accepts]: Start accepts. Automaton has 208 states and 640 transitions. Word has length 18
[2025-04-28 21:21:40,284 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,284 INFO  L485      AbstractCegarLoop]: Abstraction has 208 states and 640 transitions.
[2025-04-28 21:21:40,285 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,286 INFO  L278                IsEmpty]: Start isEmpty. Operand 208 states and 640 transitions.
[2025-04-28 21:21:40,303 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:40,306 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,306 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:40,306 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:40,307 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,308 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,308 INFO  L85        PathProgramCache]: Analyzing trace with hash 215406343, now seen corresponding path program 1 times
[2025-04-28 21:21:40,308 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,308 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [236184887]
[2025-04-28 21:21:40,309 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,309 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,323 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:40,345 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:40,345 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,345 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,564 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:40,564 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,564 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [236184887]
[2025-04-28 21:21:40,564 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [236184887] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,565 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,565 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:40,565 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [934263199]
[2025-04-28 21:21:40,565 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,566 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:40,566 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,567 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:40,567 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:40,568 INFO  L87              Difference]: Start difference. First operand 208 states and 640 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:42,063 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,064 INFO  L93              Difference]: Finished difference Result 323 states and 1447 transitions.
[2025-04-28 21:21:42,064 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:42,065 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:42,065 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,085 INFO  L225             Difference]: With dead ends: 323
[2025-04-28 21:21:42,085 INFO  L226             Difference]: Without dead ends: 323
[2025-04-28 21:21:42,086 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:42,087 INFO  L437           NwaCegarLoop]: 330 mSDtfsCounter, 8 mSDsluCounter, 1119 mSDsCounter, 0 mSdLazyCounter, 939 mSolverCounterSat, 44 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 64 SdHoareTripleChecker+Valid, 1449 SdHoareTripleChecker+Invalid, 983 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 44 IncrementalHoareTripleChecker+Valid, 939 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,087 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [64 Valid, 1449 Invalid, 983 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [44 Valid, 939 Invalid, 0 Unknown, 0 Unchecked, 1.4s Time]
[2025-04-28 21:21:42,089 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 323 states.
[2025-04-28 21:21:42,374 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 323 to 321.
[2025-04-28 21:21:42,376 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 321 states, 22 states have (on average 3.0454545454545454) internal successors, (67), 56 states have internal predecessors, (67), 291 states have call successors, (318), 12 states have call predecessors, (318), 14 states have return successors, (1060), 257 states have call predecessors, (1060), 291 states have call successors, (1060)
[2025-04-28 21:21:42,387 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 321 states to 321 states and 1445 transitions.
[2025-04-28 21:21:42,387 INFO  L79                 Accepts]: Start accepts. Automaton has 321 states and 1445 transitions. Word has length 18
[2025-04-28 21:21:42,388 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,388 INFO  L485      AbstractCegarLoop]: Abstraction has 321 states and 1445 transitions.
[2025-04-28 21:21:42,388 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:42,388 INFO  L278                IsEmpty]: Start isEmpty. Operand 321 states and 1445 transitions.
[2025-04-28 21:21:42,397 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:42,397 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,397 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:42,398 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:42,398 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,399 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,399 INFO  L85        PathProgramCache]: Analyzing trace with hash 1815844197, now seen corresponding path program 1 times
[2025-04-28 21:21:42,399 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,399 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1783775558]
[2025-04-28 21:21:42,399 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,399 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,414 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:42,437 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:42,437 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,438 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,677 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,677 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,677 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1783775558]
[2025-04-28 21:21:42,677 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1783775558] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,677 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,678 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:42,678 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [56471844]
[2025-04-28 21:21:42,678 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,678 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:42,678 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,679 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:42,679 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,679 INFO  L87              Difference]: Start difference. First operand 321 states and 1445 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:44,175 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,176 INFO  L93              Difference]: Finished difference Result 471 states and 3117 transitions.
[2025-04-28 21:21:44,176 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:44,177 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,177 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,206 INFO  L225             Difference]: With dead ends: 471
[2025-04-28 21:21:44,206 INFO  L226             Difference]: Without dead ends: 471
[2025-04-28 21:21:44,206 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,207 INFO  L437           NwaCegarLoop]: 335 mSDtfsCounter, 6 mSDsluCounter, 1139 mSDsCounter, 0 mSdLazyCounter, 905 mSolverCounterSat, 46 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 58 SdHoareTripleChecker+Valid, 1474 SdHoareTripleChecker+Invalid, 951 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 46 IncrementalHoareTripleChecker+Valid, 905 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,207 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [58 Valid, 1474 Invalid, 951 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [46 Valid, 905 Invalid, 0 Unknown, 0 Unchecked, 1.4s Time]
[2025-04-28 21:21:44,209 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 471 states.
[2025-04-28 21:21:44,663 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 471 to 469.
[2025-04-28 21:21:44,667 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 469 states, 34 states have (on average 3.0) internal successors, (102), 88 states have internal predecessors, (102), 423 states have call successors, (466), 20 states have call predecessors, (466), 22 states have return successors, (2547), 369 states have call predecessors, (2547), 423 states have call successors, (2547)
[2025-04-28 21:21:44,686 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 469 states to 469 states and 3115 transitions.
[2025-04-28 21:21:44,686 INFO  L79                 Accepts]: Start accepts. Automaton has 469 states and 3115 transitions. Word has length 18
[2025-04-28 21:21:44,686 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,686 INFO  L485      AbstractCegarLoop]: Abstraction has 469 states and 3115 transitions.
[2025-04-28 21:21:44,687 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:44,687 INFO  L278                IsEmpty]: Start isEmpty. Operand 469 states and 3115 transitions.
[2025-04-28 21:21:44,698 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 19
[2025-04-28 21:21:44,698 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,698 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:44,699 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:44,699 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,700 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,700 INFO  L85        PathProgramCache]: Analyzing trace with hash -570647677, now seen corresponding path program 1 times
[2025-04-28 21:21:44,700 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,701 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1555937977]
[2025-04-28 21:21:44,702 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,703 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,713 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 18 statements into 1 equivalence classes.
[2025-04-28 21:21:44,733 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 18 of 18 statements.
[2025-04-28 21:21:44,734 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,734 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,942 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:44,942 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,942 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1555937977]
[2025-04-28 21:21:44,943 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1555937977] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,943 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,943 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:44,943 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2133232410]
[2025-04-28 21:21:44,943 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,944 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:44,944 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,944 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:44,944 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:44,945 INFO  L87              Difference]: Start difference. First operand 469 states and 3115 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,345 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,345 INFO  L93              Difference]: Finished difference Result 545 states and 4210 transitions.
[2025-04-28 21:21:46,346 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:46,346 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,346 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,376 INFO  L225             Difference]: With dead ends: 545
[2025-04-28 21:21:46,376 INFO  L226             Difference]: Without dead ends: 545
[2025-04-28 21:21:46,377 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,377 INFO  L437           NwaCegarLoop]: 254 mSDtfsCounter, 6 mSDsluCounter, 832 mSDsCounter, 0 mSdLazyCounter, 907 mSolverCounterSat, 46 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 67 SdHoareTripleChecker+Valid, 1086 SdHoareTripleChecker+Invalid, 953 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 46 IncrementalHoareTripleChecker+Valid, 907 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,378 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [67 Valid, 1086 Invalid, 953 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [46 Valid, 907 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:46,379 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 545 states.
[2025-04-28 21:21:47,083 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 545 to 543.
[2025-04-28 21:21:47,086 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 543 states, 40 states have (on average 3.1) internal successors, (124), 102 states have internal predecessors, (124), 489 states have call successors, (540), 24 states have call predecessors, (540), 26 states have return successors, (3544), 425 states have call predecessors, (3544), 489 states have call successors, (3544)
[2025-04-28 21:21:47,116 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 543 states to 543 states and 4208 transitions.
[2025-04-28 21:21:47,116 INFO  L79                 Accepts]: Start accepts. Automaton has 543 states and 4208 transitions. Word has length 18
[2025-04-28 21:21:47,116 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,116 INFO  L485      AbstractCegarLoop]: Abstraction has 543 states and 4208 transitions.
[2025-04-28 21:21:47,117 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,117 INFO  L278                IsEmpty]: Start isEmpty. Operand 543 states and 4208 transitions.
[2025-04-28 21:21:47,133 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:47,134 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,134 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:47,134 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:47,134 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,135 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,136 INFO  L85        PathProgramCache]: Analyzing trace with hash 1969239275, now seen corresponding path program 1 times
[2025-04-28 21:21:47,136 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,136 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [275988972]
[2025-04-28 21:21:47,136 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,136 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,150 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:47,162 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:47,162 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,162 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,383 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:47,384 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,384 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [275988972]
[2025-04-28 21:21:47,384 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [275988972] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:47,384 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:47,384 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:47,384 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1724027831]
[2025-04-28 21:21:47,384 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,384 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:47,385 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,385 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:47,385 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:47,385 INFO  L87              Difference]: Start difference. First operand 543 states and 4208 transitions. Second operand  has 5 states, 4 states have (on average 1.5) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:48,640 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,640 INFO  L93              Difference]: Finished difference Result 695 states and 6593 transitions.
[2025-04-28 21:21:48,641 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:48,641 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (6), 1 states have call predecessors, (6), 3 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:48,641 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,701 INFO  L225             Difference]: With dead ends: 695
[2025-04-28 21:21:48,702 INFO  L226             Difference]: Without dead ends: 695
[2025-04-28 21:21:48,702 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:48,705 INFO  L437           NwaCegarLoop]: 292 mSDtfsCounter, 6 mSDsluCounter, 682 mSDsCounter, 0 mSdLazyCounter, 765 mSolverCounterSat, 35 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 59 SdHoareTripleChecker+Valid, 974 SdHoareTripleChecker+Invalid, 800 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 35 IncrementalHoareTripleChecker+Valid, 765 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,705 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [59 Valid, 974 Invalid, 800 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [35 Valid, 765 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:21:48,707 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 695 states.
[2025-04-28 21:21:50,576 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 695 to 683.
[2025-04-28 21:21:50,581 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 683 states, 56 states have (on average 2.6785714285714284) internal successors, (150), 126 states have internal predecessors, (150), 601 states have call successors, (660), 28 states have call predecessors, (660), 40 states have return successors, (5675), 537 states have call predecessors, (5675), 601 states have call successors, (5675)
[2025-04-28 21:21:50,623 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 683 states to 683 states and 6485 transitions.
[2025-04-28 21:21:50,623 INFO  L79                 Accepts]: Start accepts. Automaton has 683 states and 6485 transitions. Word has length 21
[2025-04-28 21:21:50,623 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,623 INFO  L485      AbstractCegarLoop]: Abstraction has 683 states and 6485 transitions.
[2025-04-28 21:21:50,624 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 4 states have (on average 1.5) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 4 states have call predecessors, (6), 2 states have call successors, (6)
[2025-04-28 21:21:50,624 INFO  L278                IsEmpty]: Start isEmpty. Operand 683 states and 6485 transitions.
[2025-04-28 21:21:50,647 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:50,648 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,648 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:50,648 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:50,648 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,649 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,649 INFO  L85        PathProgramCache]: Analyzing trace with hash 834938559, now seen corresponding path program 1 times
[2025-04-28 21:21:50,649 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,649 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2057020221]
[2025-04-28 21:21:50,649 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,650 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,659 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:50,671 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:50,672 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,672 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,904 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:21:50,904 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,904 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2057020221]
[2025-04-28 21:21:50,904 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2057020221] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,904 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,905 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:50,905 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [215573337]
[2025-04-28 21:21:50,905 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,905 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:50,905 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,906 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:50,906 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:50,907 INFO  L87              Difference]: Start difference. First operand 683 states and 6485 transitions. Second operand  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 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:21:52,393 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,393 INFO  L93              Difference]: Finished difference Result 1009 states and 13090 transitions.
[2025-04-28 21:21:52,394 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:52,394 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 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:21:52,394 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,478 INFO  L225             Difference]: With dead ends: 1009
[2025-04-28 21:21:52,479 INFO  L226             Difference]: Without dead ends: 1009
[2025-04-28 21:21:52,479 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:21:52,479 INFO  L437           NwaCegarLoop]: 288 mSDtfsCounter, 11 mSDsluCounter, 942 mSDsCounter, 0 mSdLazyCounter, 1025 mSolverCounterSat, 69 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 105 SdHoareTripleChecker+Valid, 1230 SdHoareTripleChecker+Invalid, 1094 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 69 IncrementalHoareTripleChecker+Valid, 1025 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,480 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [105 Valid, 1230 Invalid, 1094 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [69 Valid, 1025 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:52,481 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1009 states.
[2025-04-28 21:21:54,658 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1009 to 975.
[2025-04-28 21:21:54,667 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 975 states, 82 states have (on average 2.6097560975609757) internal successors, (214), 180 states have internal predecessors, (214), 855 states have call successors, (941), 41 states have call predecessors, (941), 59 states have return successors, (11577), 762 states have call predecessors, (11577), 855 states have call successors, (11577)
[2025-04-28 21:21:54,756 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 975 states to 975 states and 12732 transitions.
[2025-04-28 21:21:54,756 INFO  L79                 Accepts]: Start accepts. Automaton has 975 states and 12732 transitions. Word has length 21
[2025-04-28 21:21:54,756 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,756 INFO  L485      AbstractCegarLoop]: Abstraction has 975 states and 12732 transitions.
[2025-04-28 21:21:54,756 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.4) internal successors, (7), 4 states have internal predecessors, (7), 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:21:54,756 INFO  L278                IsEmpty]: Start isEmpty. Operand 975 states and 12732 transitions.
[2025-04-28 21:21:54,784 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:54,784 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,784 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:21:54,785 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:54,785 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,786 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,786 INFO  L85        PathProgramCache]: Analyzing trace with hash 1930976911, now seen corresponding path program 1 times
[2025-04-28 21:21:54,786 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,786 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1170545061]
[2025-04-28 21:21:54,786 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,786 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,798 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:54,813 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:54,814 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,814 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,105 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:21:55,105 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,105 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1170545061]
[2025-04-28 21:21:55,107 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1170545061] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:55,107 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:55,107 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:55,107 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [396625075]
[2025-04-28 21:21:55,107 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,108 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:55,108 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,108 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:55,108 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:55,109 INFO  L87              Difference]: Start difference. First operand 975 states and 12732 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:21:56,918 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,918 INFO  L93              Difference]: Finished difference Result 1475 states and 26951 transitions.
[2025-04-28 21:21:56,918 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:56,918 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:21:56,919 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,112 INFO  L225             Difference]: With dead ends: 1475
[2025-04-28 21:21:57,112 INFO  L226             Difference]: Without dead ends: 1475
[2025-04-28 21:21:57,112 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:21:57,113 INFO  L437           NwaCegarLoop]: 253 mSDtfsCounter, 11 mSDsluCounter, 819 mSDsCounter, 0 mSdLazyCounter, 1022 mSolverCounterSat, 68 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 115 SdHoareTripleChecker+Valid, 1072 SdHoareTripleChecker+Invalid, 1090 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 68 IncrementalHoareTripleChecker+Valid, 1022 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.5s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,113 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [115 Valid, 1072 Invalid, 1090 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [68 Valid, 1022 Invalid, 0 Unknown, 0 Unchecked, 1.5s Time]
[2025-04-28 21:21:57,116 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 1475 states.
[2025-04-28 21:22:01,043 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 1475 to 1441.
[2025-04-28 21:22:01,059 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 1441 states, 118 states have (on average 2.6779661016949152) internal successors, (316), 264 states have internal predecessors, (316), 1273 states have call successors, (1405), 63 states have call predecessors, (1405), 83 states have return successors, (24720), 1122 states have call predecessors, (24720), 1273 states have call successors, (24720)
[2025-04-28 21:22:01,262 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 1441 states to 1441 states and 26441 transitions.
[2025-04-28 21:22:01,262 INFO  L79                 Accepts]: Start accepts. Automaton has 1441 states and 26441 transitions. Word has length 21
[2025-04-28 21:22:01,263 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,263 INFO  L485      AbstractCegarLoop]: Abstraction has 1441 states and 26441 transitions.
[2025-04-28 21:22:01,263 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, (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:01,263 INFO  L278                IsEmpty]: Start isEmpty. Operand 1441 states and 26441 transitions.
[2025-04-28 21:22:01,291 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:22:01,291 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,291 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:01,291 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:22:01,291 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,293 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,293 INFO  L85        PathProgramCache]: Analyzing trace with hash -1577936365, now seen corresponding path program 1 times
[2025-04-28 21:22:01,293 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,293 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [914810816]
[2025-04-28 21:22:01,293 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,293 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,304 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:22:01,313 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:22:01,315 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,315 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,531 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:01,531 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,532 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [914810816]
[2025-04-28 21:22:01,532 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [914810816] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:01,532 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:01,532 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:22:01,532 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [650890987]
[2025-04-28 21:22:01,532 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,532 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:22:01,533 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,533 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:22:01,533 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:22:01,533 INFO  L87              Difference]: Start difference. First operand 1441 states and 26441 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:03,178 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:03,179 INFO  L93              Difference]: Finished difference Result 2071 states and 52461 transitions.
[2025-04-28 21:22:03,179 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:22:03,180 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:03,180 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:03,778 INFO  L225             Difference]: With dead ends: 2071
[2025-04-28 21:22:03,778 INFO  L226             Difference]: Without dead ends: 2071
[2025-04-28 21:22:03,779 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:03,780 INFO  L437           NwaCegarLoop]: 305 mSDtfsCounter, 8 mSDsluCounter, 1047 mSDsCounter, 0 mSdLazyCounter, 886 mSolverCounterSat, 42 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 63 SdHoareTripleChecker+Valid, 1352 SdHoareTripleChecker+Invalid, 928 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 42 IncrementalHoareTripleChecker+Valid, 886 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:03,780 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [63 Valid, 1352 Invalid, 928 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [42 Valid, 886 Invalid, 0 Unknown, 0 Unchecked, 1.1s Time]
[2025-04-28 21:22:03,783 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 2071 states.
