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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:21,928 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:22,029 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8235c6f8-b6ed-4e6f-94fc-4d7ba13606c1/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:22,039 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:22,039 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:22,072 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:22,072 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:22,072 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:22,073 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:22,074 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:22,076 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:22,076 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:22,076 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:22,076 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:22,077 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:22,077 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:22,078 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:22,078 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:22,078 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:22,078 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:22,078 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:22,078 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:22,079 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:22,079 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:22,079 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:22,080 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:22,080 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:22,425 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:22,437 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:22,439 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:22,442 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:22,443 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:22,444 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8235c6f8-b6ed-4e6f-94fc-4d7ba13606c1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-159.smt2
[2025-04-28 21:21:22,447 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:22,454 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:22,735 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8235c6f8-b6ed-4e6f-94fc-4d7ba13606c1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-159.smt2
[2025-04-28 21:21:22,739 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:22,741 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:22,743 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:22,743 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:22,743 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:22,746 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,777 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22 Unit
[2025-04-28 21:21:22,777 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:22,778 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:22,778 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:22,778 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:22,796 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,796 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,827 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,828 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,831 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,834 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,839 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,840 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,843 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,861 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:22,862 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:22,862 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:22,862 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:22,863 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (1/1) ...
[2025-04-28 21:21:22,866 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:22,884 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:22,898 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:22,903 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:22,918 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:22,918 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:22,918 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:22,918 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_3 given in one single declaration
[2025-04-28 21:21:22,918 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_3
[2025-04-28 21:21:22,918 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_3
[2025-04-28 21:21:22,919 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_2 given in one single declaration
[2025-04-28 21:21:22,919 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_2
[2025-04-28 21:21:22,920 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_2
[2025-04-28 21:21:22,920 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:22,920 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:22,920 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:22,920 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:22,920 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:22,920 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:22,981 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:22,983 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:23,276 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:23,276 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:23,291 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:23,292 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:23,293 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:23 BoogieIcfgContainer
[2025-04-28 21:21:23,293 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:23,296 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:23,296 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:23,300 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:23,301 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:22" (1/3) ...
[2025-04-28 21:21:23,301 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@42d729f6 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:23, skipping insertion in model container
[2025-04-28 21:21:23,302 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:22" (2/3) ...
[2025-04-28 21:21:23,302 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@42d729f6 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:23, skipping insertion in model container
[2025-04-28 21:21:23,302 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:23" (3/3) ...
[2025-04-28 21:21:23,304 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:23,320 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:23,322 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 5 procedures, 29 locations, 59 edges, 5 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:23,369 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:23,390 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;@682e67cd, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:23,390 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:23,394 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 29 states, 10 states have (on average 2.0) internal successors, (20), 20 states have internal predecessors, (20), 13 states have call successors, (13), 4 states have call predecessors, (13), 4 states have return successors, (13), 5 states have call predecessors, (13), 13 states have call successors, (13)
[2025-04-28 21:21:23,409 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 18
[2025-04-28 21:21:23,410 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,411 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:23,412 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,419 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,419 INFO  L85        PathProgramCache]: Analyzing trace with hash -1004432503, now seen corresponding path program 1 times
[2025-04-28 21:21:23,427 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,428 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1660842380]
[2025-04-28 21:21:23,428 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,429 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,477 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 17 statements into 1 equivalence classes.
[2025-04-28 21:21:23,506 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 17 of 17 statements.
[2025-04-28 21:21:23,506 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,507 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,782 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:23,783 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,783 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1660842380]
[2025-04-28 21:21:23,784 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1660842380] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:23,784 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:23,788 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:23,789 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1105522140]
[2025-04-28 21:21:23,790 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:23,798 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:23,798 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:23,829 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:23,829 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:23,831 INFO  L87              Difference]: Start difference. First operand  has 29 states, 10 states have (on average 2.0) internal successors, (20), 20 states have internal predecessors, (20), 13 states have call successors, (13), 4 states have call predecessors, (13), 4 states have return successors, (13), 5 states have call predecessors, (13), 13 states have call successors, (13) Second operand  has 6 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 2 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:24,047 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:24,048 INFO  L93              Difference]: Finished difference Result 33 states and 58 transitions.
[2025-04-28 21:21:24,049 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:24,051 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 2 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 2 states have call successors, (4) Word has length 17
[2025-04-28 21:21:24,052 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:24,059 INFO  L225             Difference]: With dead ends: 33
[2025-04-28 21:21:24,059 INFO  L226             Difference]: Without dead ends: 33
[2025-04-28 21:21:24,061 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:24,066 INFO  L437           NwaCegarLoop]: 33 mSDtfsCounter, 1 mSDsluCounter, 109 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 142 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:24,091 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 142 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:24,107 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 33 states.
[2025-04-28 21:21:24,158 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 33 to 33.
[2025-04-28 21:21:24,160 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 33 states, 12 states have (on average 1.75) internal successors, (21), 21 states have internal predecessors, (21), 13 states have call successors, (13), 4 states have call predecessors, (13), 7 states have return successors, (24), 7 states have call predecessors, (24), 13 states have call successors, (24)
[2025-04-28 21:21:24,164 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 33 states to 33 states and 58 transitions.
[2025-04-28 21:21:24,166 INFO  L79                 Accepts]: Start accepts. Automaton has 33 states and 58 transitions. Word has length 17
[2025-04-28 21:21:24,168 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:24,169 INFO  L485      AbstractCegarLoop]: Abstraction has 33 states and 58 transitions.
[2025-04-28 21:21:24,169 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 1.8) internal successors, (9), 6 states have internal predecessors, (9), 2 states have call successors, (4), 1 states have call predecessors, (4), 4 states have return successors, (4), 3 states have call predecessors, (4), 2 states have call successors, (4)
[2025-04-28 21:21:24,170 INFO  L278                IsEmpty]: Start isEmpty. Operand 33 states and 58 transitions.
[2025-04-28 21:21:24,174 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:24,174 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:24,174 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:24,174 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:24,175 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:24,176 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:24,176 INFO  L85        PathProgramCache]: Analyzing trace with hash -1999835381, now seen corresponding path program 1 times
[2025-04-28 21:21:24,176 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:24,176 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1452457604]
[2025-04-28 21:21:24,176 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,177 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:24,186 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:24,207 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:24,207 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,207 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,491 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,492 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,492 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1452457604]
[2025-04-28 21:21:24,492 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1452457604] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:24,492 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1626293947]
[2025-04-28 21:21:24,493 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,493 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:24,496 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:24,502 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,508 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,564 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:24,601 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:24,603 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,603 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,608 INFO  L256         TraceCheckSpWp]: Trace formula consists of 107 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:24,615 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:24,768 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,768 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:25,402 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:25,403 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1626293947] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:25,404 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:25,404 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:25,405 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [635561478]
[2025-04-28 21:21:25,406 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,406 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:25,407 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,408 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:25,409 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:25,409 INFO  L87              Difference]: Start difference. First operand 33 states and 58 transitions. Second operand  has 12 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:25,715 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,715 INFO  L93              Difference]: Finished difference Result 45 states and 87 transitions.
[2025-04-28 21:21:25,716 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:25,717 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10) Word has length 21
[2025-04-28 21:21:25,717 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,719 INFO  L225             Difference]: With dead ends: 45
[2025-04-28 21:21:25,720 INFO  L226             Difference]: Without dead ends: 45
[2025-04-28 21:21:25,721 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 50 GetRequests, 36 SyntacticMatches, 3 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 15 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:25,724 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 5 mSDsluCounter, 215 mSDsCounter, 0 mSdLazyCounter, 152 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 253 SdHoareTripleChecker+Invalid, 168 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 152 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:25,724 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 253 Invalid, 168 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 152 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:25,725 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 45 states.
[2025-04-28 21:21:25,745 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 45 to 39.
[2025-04-28 21:21:25,745 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 39 states, 15 states have (on average 1.6) internal successors, (24), 24 states have internal predecessors, (24), 13 states have call successors, (13), 4 states have call predecessors, (13), 10 states have return successors, (35), 10 states have call predecessors, (35), 13 states have call successors, (35)
[2025-04-28 21:21:25,747 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 39 states to 39 states and 72 transitions.
[2025-04-28 21:21:25,747 INFO  L79                 Accepts]: Start accepts. Automaton has 39 states and 72 transitions. Word has length 21
[2025-04-28 21:21:25,747 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,747 INFO  L485      AbstractCegarLoop]: Abstraction has 39 states and 72 transitions.
[2025-04-28 21:21:25,747 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:25,748 INFO  L278                IsEmpty]: Start isEmpty. Operand 39 states and 72 transitions.
[2025-04-28 21:21:25,751 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:25,753 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,753 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:25,760 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:25,954 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,954 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,955 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,955 INFO  L85        PathProgramCache]: Analyzing trace with hash 741914867, now seen corresponding path program 1 times
[2025-04-28 21:21:25,955 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,955 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [264825961]
[2025-04-28 21:21:25,955 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,956 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,962 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:25,975 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:25,975 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,976 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,130 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:26,130 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,131 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [264825961]
[2025-04-28 21:21:26,131 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [264825961] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:26,131 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:26,131 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:26,131 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [42198356]
[2025-04-28 21:21:26,131 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,132 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:26,132 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,132 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:26,133 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:26,133 INFO  L87              Difference]: Start difference. First operand 39 states and 72 transitions. Second operand  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:26,390 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,391 INFO  L93              Difference]: Finished difference Result 57 states and 115 transitions.
[2025-04-28 21:21:26,393 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:26,393 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 21
[2025-04-28 21:21:26,394 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,399 INFO  L225             Difference]: With dead ends: 57
[2025-04-28 21:21:26,400 INFO  L226             Difference]: Without dead ends: 57
[2025-04-28 21:21:26,400 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:26,401 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 6 mSDsluCounter, 122 mSDsCounter, 0 mSdLazyCounter, 126 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 165 SdHoareTripleChecker+Invalid, 131 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 126 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,401 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 165 Invalid, 131 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 126 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:26,404 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 57 states.
[2025-04-28 21:21:26,432 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 57 to 51.
[2025-04-28 21:21:26,432 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 51 states, 20 states have (on average 1.6) internal successors, (32), 31 states have internal predecessors, (32), 16 states have call successors, (16), 5 states have call predecessors, (16), 14 states have return successors, (50), 14 states have call predecessors, (50), 16 states have call successors, (50)
[2025-04-28 21:21:26,436 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 51 states to 51 states and 98 transitions.
[2025-04-28 21:21:26,437 INFO  L79                 Accepts]: Start accepts. Automaton has 51 states and 98 transitions. Word has length 21
[2025-04-28 21:21:26,439 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,439 INFO  L485      AbstractCegarLoop]: Abstraction has 51 states and 98 transitions.
[2025-04-28 21:21:26,439 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:26,439 INFO  L278                IsEmpty]: Start isEmpty. Operand 51 states and 98 transitions.
[2025-04-28 21:21:26,443 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:26,444 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,444 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:26,444 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:26,444 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,445 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,445 INFO  L85        PathProgramCache]: Analyzing trace with hash -1706908565, now seen corresponding path program 1 times
[2025-04-28 21:21:26,445 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,445 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [912383624]
[2025-04-28 21:21:26,445 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,445 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,457 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:26,472 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:26,472 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,472 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,620 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:26,620 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:26,621 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [912383624]
[2025-04-28 21:21:26,621 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [912383624] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:26,621 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:26,621 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:26,621 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [522325067]
[2025-04-28 21:21:26,622 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,622 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:26,622 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,623 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:26,623 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:26,623 INFO  L87              Difference]: Start difference. First operand 51 states and 98 transitions. Second operand  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:26,772 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:26,772 INFO  L93              Difference]: Finished difference Result 69 states and 139 transitions.
[2025-04-28 21:21:26,772 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:26,773 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 21
[2025-04-28 21:21:26,773 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:26,774 INFO  L225             Difference]: With dead ends: 69
[2025-04-28 21:21:26,775 INFO  L226             Difference]: Without dead ends: 67
[2025-04-28 21:21:26,775 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:26,776 INFO  L437           NwaCegarLoop]: 39 mSDtfsCounter, 3 mSDsluCounter, 121 mSDsCounter, 0 mSdLazyCounter, 83 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 160 SdHoareTripleChecker+Invalid, 86 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 83 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:26,776 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 160 Invalid, 86 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 83 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:26,777 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 67 states.
[2025-04-28 21:21:26,789 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 67 to 59.
[2025-04-28 21:21:26,789 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 59 states, 24 states have (on average 1.5) internal successors, (36), 35 states have internal predecessors, (36), 16 states have call successors, (16), 5 states have call predecessors, (16), 18 states have return successors, (63), 18 states have call predecessors, (63), 16 states have call successors, (63)
[2025-04-28 21:21:26,791 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 59 states to 59 states and 115 transitions.
[2025-04-28 21:21:26,791 INFO  L79                 Accepts]: Start accepts. Automaton has 59 states and 115 transitions. Word has length 21
[2025-04-28 21:21:26,791 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:26,791 INFO  L485      AbstractCegarLoop]: Abstraction has 59 states and 115 transitions.
[2025-04-28 21:21:26,792 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:26,792 INFO  L278                IsEmpty]: Start isEmpty. Operand 59 states and 115 transitions.
[2025-04-28 21:21:26,793 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:26,794 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:26,794 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:26,794 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:26,794 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:26,795 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:26,795 INFO  L85        PathProgramCache]: Analyzing trace with hash -1980162056, now seen corresponding path program 1 times
[2025-04-28 21:21:26,795 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:26,795 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [910156575]
[2025-04-28 21:21:26,795 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:26,795 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:26,800 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:26,809 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:26,810 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,810 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,112 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:27,112 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,112 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [910156575]
[2025-04-28 21:21:27,113 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [910156575] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,113 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1449962718]
[2025-04-28 21:21:27,113 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,113 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,116 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,118 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:27,121 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:27,170 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:27,192 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:27,192 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,192 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,194 INFO  L256         TraceCheckSpWp]: Trace formula consists of 103 conjuncts, 27 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:27,195 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:27,417 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:27,417 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:28,263 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:28,263 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1449962718] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:28,263 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:28,265 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 9] total 19
[2025-04-28 21:21:28,265 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [321523858]
[2025-04-28 21:21:28,265 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:28,265 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:28,265 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:28,266 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:28,266 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=289, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:28,266 INFO  L87              Difference]: Start difference. First operand 59 states and 115 transitions. Second operand  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 7 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:21:28,786 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:28,786 INFO  L93              Difference]: Finished difference Result 77 states and 161 transitions.
[2025-04-28 21:21:28,786 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:28,787 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 7 states have call predecessors, (12), 11 states have call successors, (12) Word has length 21
[2025-04-28 21:21:28,787 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:28,789 INFO  L225             Difference]: With dead ends: 77
[2025-04-28 21:21:28,789 INFO  L226             Difference]: Without dead ends: 77
[2025-04-28 21:21:28,790 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 55 GetRequests, 34 SyntacticMatches, 0 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 60 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=78, Invalid=428, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:28,790 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 11 mSDsluCounter, 311 mSDsCounter, 0 mSdLazyCounter, 347 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 347 SdHoareTripleChecker+Invalid, 363 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 347 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:28,791 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 347 Invalid, 363 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 347 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:28,792 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 77 states.
[2025-04-28 21:21:28,814 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 77 to 63.
[2025-04-28 21:21:28,814 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 63 states, 26 states have (on average 1.4615384615384615) internal successors, (38), 37 states have internal predecessors, (38), 16 states have call successors, (16), 5 states have call predecessors, (16), 20 states have return successors, (71), 20 states have call predecessors, (71), 16 states have call successors, (71)
[2025-04-28 21:21:28,819 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 63 states to 63 states and 125 transitions.
[2025-04-28 21:21:28,819 INFO  L79                 Accepts]: Start accepts. Automaton has 63 states and 125 transitions. Word has length 21
[2025-04-28 21:21:28,820 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:28,820 INFO  L485      AbstractCegarLoop]: Abstraction has 63 states and 125 transitions.
[2025-04-28 21:21:28,820 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 19 states have internal predecessors, (21), 11 states have call successors, (12), 1 states have call predecessors, (12), 8 states have return successors, (12), 7 states have call predecessors, (12), 11 states have call successors, (12)
[2025-04-28 21:21:28,820 INFO  L278                IsEmpty]: Start isEmpty. Operand 63 states and 125 transitions.
[2025-04-28 21:21:28,822 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:28,822 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:28,825 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:28,830 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:29,025 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,026 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,026 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,026 INFO  L85        PathProgramCache]: Analyzing trace with hash -1331568360, now seen corresponding path program 1 times
[2025-04-28 21:21:29,026 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,026 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [829949229]
[2025-04-28 21:21:29,027 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,027 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,032 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:29,037 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:29,037 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,038 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,110 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:29,110 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,110 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [829949229]
[2025-04-28 21:21:29,110 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [829949229] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:29,111 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:29,111 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:29,111 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1723866016]
[2025-04-28 21:21:29,112 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,112 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:29,112 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,113 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:29,113 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:29,113 INFO  L87              Difference]: Start difference. First operand 63 states and 125 transitions. Second operand  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:29,293 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:29,293 INFO  L93              Difference]: Finished difference Result 73 states and 137 transitions.
[2025-04-28 21:21:29,294 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:29,294 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5) Word has length 21
[2025-04-28 21:21:29,294 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:29,296 INFO  L225             Difference]: With dead ends: 73
[2025-04-28 21:21:29,296 INFO  L226             Difference]: Without dead ends: 67
[2025-04-28 21:21:29,296 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:29,297 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 6 mSDsluCounter, 118 mSDsCounter, 0 mSdLazyCounter, 124 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 160 SdHoareTripleChecker+Invalid, 131 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 124 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:29,297 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 160 Invalid, 131 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 124 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:29,298 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 67 states.
[2025-04-28 21:21:29,315 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 67 to 55.
[2025-04-28 21:21:29,318 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 55 states, 22 states have (on average 1.5454545454545454) internal successors, (34), 33 states have internal predecessors, (34), 16 states have call successors, (16), 5 states have call predecessors, (16), 16 states have return successors, (55), 16 states have call predecessors, (55), 16 states have call successors, (55)
[2025-04-28 21:21:29,319 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 55 states to 55 states and 105 transitions.
[2025-04-28 21:21:29,321 INFO  L79                 Accepts]: Start accepts. Automaton has 55 states and 105 transitions. Word has length 21
[2025-04-28 21:21:29,321 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:29,321 INFO  L485      AbstractCegarLoop]: Abstraction has 55 states and 105 transitions.
[2025-04-28 21:21:29,321 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 2.75) internal successors, (11), 6 states have internal predecessors, (11), 4 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:29,321 INFO  L278                IsEmpty]: Start isEmpty. Operand 55 states and 105 transitions.
[2025-04-28 21:21:29,322 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:29,322 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:29,323 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:29,323 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:29,323 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:29,323 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:29,323 INFO  L85        PathProgramCache]: Analyzing trace with hash 1620977454, now seen corresponding path program 1 times
[2025-04-28 21:21:29,324 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:29,325 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [496027603]
[2025-04-28 21:21:29,326 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,326 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:29,333 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:29,341 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:29,344 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,344 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,439 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:29,439 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:29,439 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [496027603]
[2025-04-28 21:21:29,439 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [496027603] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:29,439 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1638540345]
[2025-04-28 21:21:29,440 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:29,440 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:29,443 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:29,445 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:29,448 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:29,487 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:29,503 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:29,504 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:29,504 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:29,505 INFO  L256         TraceCheckSpWp]: Trace formula consists of 103 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:29,506 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:29,570 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:29,570 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:29,992 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:29,993 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1638540345] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:29,993 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:29,993 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:29,993 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1327171325]
[2025-04-28 21:21:29,994 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:29,995 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:29,995 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:29,996 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:29,997 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:29,997 INFO  L87              Difference]: Start difference. First operand 55 states and 105 transitions. Second operand  has 12 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:30,209 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,209 INFO  L93              Difference]: Finished difference Result 69 states and 132 transitions.
[2025-04-28 21:21:30,210 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:30,210 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10) Word has length 21
[2025-04-28 21:21:30,210 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,211 INFO  L225             Difference]: With dead ends: 69
[2025-04-28 21:21:30,211 INFO  L226             Difference]: Without dead ends: 67
[2025-04-28 21:21:30,212 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 50 GetRequests, 36 SyntacticMatches, 3 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 15 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:30,212 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 4 mSDsluCounter, 272 mSDsCounter, 0 mSdLazyCounter, 173 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 310 SdHoareTripleChecker+Invalid, 186 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 173 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,212 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 310 Invalid, 186 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 173 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:30,215 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 67 states.
[2025-04-28 21:21:30,228 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 67 to 55.
[2025-04-28 21:21:30,230 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 55 states, 22 states have (on average 1.5454545454545454) internal successors, (34), 33 states have internal predecessors, (34), 16 states have call successors, (16), 5 states have call predecessors, (16), 16 states have return successors, (53), 16 states have call predecessors, (53), 16 states have call successors, (53)
[2025-04-28 21:21:30,232 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 55 states to 55 states and 103 transitions.
[2025-04-28 21:21:30,233 INFO  L79                 Accepts]: Start accepts. Automaton has 55 states and 103 transitions. Word has length 21
[2025-04-28 21:21:30,233 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,233 INFO  L485      AbstractCegarLoop]: Abstraction has 55 states and 103 transitions.
[2025-04-28 21:21:30,234 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.5) internal successors, (15), 12 states have internal predecessors, (15), 8 states have call successors, (8), 1 states have call predecessors, (8), 6 states have return successors, (10), 5 states have call predecessors, (10), 8 states have call successors, (10)
[2025-04-28 21:21:30,236 INFO  L278                IsEmpty]: Start isEmpty. Operand 55 states and 103 transitions.
[2025-04-28 21:21:30,237 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:30,237 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,237 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:30,245 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:30,438 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:30,438 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,438 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,438 INFO  L85        PathProgramCache]: Analyzing trace with hash -354220851, now seen corresponding path program 1 times
[2025-04-28 21:21:30,439 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,439 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1574332441]
[2025-04-28 21:21:30,439 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,439 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,442 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:30,446 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:30,446 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,446 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,518 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:30,518 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,519 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1574332441]
[2025-04-28 21:21:30,519 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1574332441] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,519 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:30,519 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:30,519 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2030008009]
[2025-04-28 21:21:30,519 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,519 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:30,520 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,520 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:30,520 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:30,521 INFO  L87              Difference]: Start difference. First operand 55 states and 103 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:30,649 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,649 INFO  L93              Difference]: Finished difference Result 63 states and 119 transitions.
[2025-04-28 21:21:30,650 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:30,650 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-04-28 21:21:30,650 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,651 INFO  L225             Difference]: With dead ends: 63
[2025-04-28 21:21:30,651 INFO  L226             Difference]: Without dead ends: 61
[2025-04-28 21:21:30,652 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:30,652 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 3 mSDsluCounter, 174 mSDsCounter, 0 mSdLazyCounter, 98 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 216 SdHoareTripleChecker+Invalid, 99 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 98 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,652 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 216 Invalid, 99 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 98 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:30,653 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 61 states.
[2025-04-28 21:21:30,666 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 61 to 59.
[2025-04-28 21:21:30,668 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 59 states, 24 states have (on average 1.5) internal successors, (36), 35 states have internal predecessors, (36), 16 states have call successors, (16), 5 states have call predecessors, (16), 18 states have return successors, (60), 18 states have call predecessors, (60), 16 states have call successors, (60)
[2025-04-28 21:21:30,669 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 59 states to 59 states and 112 transitions.
[2025-04-28 21:21:30,669 INFO  L79                 Accepts]: Start accepts. Automaton has 59 states and 112 transitions. Word has length 21
[2025-04-28 21:21:30,669 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,669 INFO  L485      AbstractCegarLoop]: Abstraction has 59 states and 112 transitions.
[2025-04-28 21:21:30,669 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:30,669 INFO  L278                IsEmpty]: Start isEmpty. Operand 59 states and 112 transitions.
[2025-04-28 21:21:30,670 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:30,671 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,671 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:30,671 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:30,671 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,671 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,671 INFO  L85        PathProgramCache]: Analyzing trace with hash -1928903145, now seen corresponding path program 1 times
[2025-04-28 21:21:30,671 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,671 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1352854556]
[2025-04-28 21:21:30,671 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,672 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,678 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:30,681 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:30,681 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,681 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:30,808 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:30,809 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:30,809 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1352854556]
[2025-04-28 21:21:30,809 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1352854556] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:30,809 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:30,809 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:30,809 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [424862897]
[2025-04-28 21:21:30,810 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,810 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:30,810 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,810 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:30,811 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:30,811 INFO  L87              Difference]: Start difference. First operand 59 states and 112 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:30,957 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:30,958 INFO  L93              Difference]: Finished difference Result 67 states and 128 transitions.
[2025-04-28 21:21:30,960 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:30,960 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-04-28 21:21:30,961 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:30,962 INFO  L225             Difference]: With dead ends: 67
[2025-04-28 21:21:30,962 INFO  L226             Difference]: Without dead ends: 65
[2025-04-28 21:21:30,962 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:30,963 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 3 mSDsluCounter, 165 mSDsCounter, 0 mSdLazyCounter, 99 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 205 SdHoareTripleChecker+Invalid, 99 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 99 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:30,964 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 205 Invalid, 99 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 99 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:30,965 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 65 states.
[2025-04-28 21:21:30,973 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 65 to 61.
[2025-04-28 21:21:30,973 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 61 states, 25 states have (on average 1.48) internal successors, (37), 36 states have internal predecessors, (37), 16 states have call successors, (16), 5 states have call predecessors, (16), 19 states have return successors, (64), 19 states have call predecessors, (64), 16 states have call successors, (64)
[2025-04-28 21:21:30,975 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 61 states to 61 states and 117 transitions.
[2025-04-28 21:21:30,975 INFO  L79                 Accepts]: Start accepts. Automaton has 61 states and 117 transitions. Word has length 21
[2025-04-28 21:21:30,975 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:30,975 INFO  L485      AbstractCegarLoop]: Abstraction has 61 states and 117 transitions.
[2025-04-28 21:21:30,976 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:30,976 INFO  L278                IsEmpty]: Start isEmpty. Operand 61 states and 117 transitions.
[2025-04-28 21:21:30,977 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:30,977 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:30,977 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:30,977 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:30,977 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:30,978 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:30,978 INFO  L85        PathProgramCache]: Analyzing trace with hash -1141561998, now seen corresponding path program 1 times
[2025-04-28 21:21:30,978 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:30,978 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [875103021]
[2025-04-28 21:21:30,978 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:30,978 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:30,984 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 21 statements into 1 equivalence classes.
[2025-04-28 21:21:30,987 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:30,987 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:30,987 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,054 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:31,054 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,054 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [875103021]
[2025-04-28 21:21:31,054 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [875103021] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:31,054 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:31,054 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:31,054 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [273225668]
[2025-04-28 21:21:31,055 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,055 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:31,055 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,055 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:31,055 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:31,056 INFO  L87              Difference]: Start difference. First operand 61 states and 117 transitions. Second operand  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:31,172 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,173 INFO  L93              Difference]: Finished difference Result 71 states and 138 transitions.
[2025-04-28 21:21:31,173 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:31,174 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5) Word has length 21
[2025-04-28 21:21:31,174 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,175 INFO  L225             Difference]: With dead ends: 71
[2025-04-28 21:21:31,175 INFO  L226             Difference]: Without dead ends: 69
[2025-04-28 21:21:31,175 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:31,176 INFO  L437           NwaCegarLoop]: 37 mSDtfsCounter, 3 mSDsluCounter, 145 mSDsCounter, 0 mSdLazyCounter, 97 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 182 SdHoareTripleChecker+Invalid, 99 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 97 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,177 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 182 Invalid, 99 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 97 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:31,178 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 69 states.
[2025-04-28 21:21:31,191 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 69 to 63.
[2025-04-28 21:21:31,191 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 63 states, 26 states have (on average 1.4615384615384615) internal successors, (38), 37 states have internal predecessors, (38), 16 states have call successors, (16), 5 states have call predecessors, (16), 20 states have return successors, (68), 20 states have call predecessors, (68), 16 states have call successors, (68)
[2025-04-28 21:21:31,192 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 63 states to 63 states and 122 transitions.
[2025-04-28 21:21:31,192 INFO  L79                 Accepts]: Start accepts. Automaton has 63 states and 122 transitions. Word has length 21
[2025-04-28 21:21:31,192 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,192 INFO  L485      AbstractCegarLoop]: Abstraction has 63 states and 122 transitions.
[2025-04-28 21:21:31,193 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.0) internal successors, (10), 7 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 4 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:31,193 INFO  L278                IsEmpty]: Start isEmpty. Operand 63 states and 122 transitions.
[2025-04-28 21:21:31,194 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:31,194 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,194 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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:31,194 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:31,195 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,195 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,195 INFO  L85        PathProgramCache]: Analyzing trace with hash 19201781, now seen corresponding path program 1 times
[2025-04-28 21:21:31,195 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,195 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [145878410]
[2025-04-28 21:21:31,195 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,196 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,200 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:31,206 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:31,206 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,206 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,295 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:31,295 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,295 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [145878410]
[2025-04-28 21:21:31,295 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [145878410] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:31,295 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:31,296 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:31,296 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1542384616]
[2025-04-28 21:21:31,296 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:31,296 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:31,296 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:31,297 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:31,297 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:31,297 INFO  L87              Difference]: Start difference. First operand 63 states and 122 transitions. Second operand  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:31,584 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:31,584 INFO  L93              Difference]: Finished difference Result 87 states and 165 transitions.
[2025-04-28 21:21:31,584 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:31,585 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6) Word has length 25
[2025-04-28 21:21:31,585 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:31,586 INFO  L225             Difference]: With dead ends: 87
[2025-04-28 21:21:31,586 INFO  L226             Difference]: Without dead ends: 87
[2025-04-28 21:21:31,587 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=100, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:31,587 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 7 mSDsluCounter, 157 mSDsCounter, 0 mSdLazyCounter, 228 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 195 SdHoareTripleChecker+Invalid, 240 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 228 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:31,588 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 195 Invalid, 240 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 228 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:31,588 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 87 states.
[2025-04-28 21:21:31,598 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 87 to 71.
[2025-04-28 21:21:31,602 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 71 states, 30 states have (on average 1.4) internal successors, (42), 41 states have internal predecessors, (42), 16 states have call successors, (16), 5 states have call predecessors, (16), 24 states have return successors, (82), 24 states have call predecessors, (82), 16 states have call successors, (82)
[2025-04-28 21:21:31,603 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 71 states to 71 states and 140 transitions.
[2025-04-28 21:21:31,603 INFO  L79                 Accepts]: Start accepts. Automaton has 71 states and 140 transitions. Word has length 25
[2025-04-28 21:21:31,603 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:31,604 INFO  L485      AbstractCegarLoop]: Abstraction has 71 states and 140 transitions.
[2025-04-28 21:21:31,604 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:31,604 INFO  L278                IsEmpty]: Start isEmpty. Operand 71 states and 140 transitions.
[2025-04-28 21:21:31,605 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:31,609 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:31,609 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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:31,609 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:31,609 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:31,610 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:31,610 INFO  L85        PathProgramCache]: Analyzing trace with hash 1139588506, now seen corresponding path program 1 times
[2025-04-28 21:21:31,610 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:31,610 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1351771111]
[2025-04-28 21:21:31,610 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,610 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:31,614 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:31,624 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:31,626 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,626 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,716 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:31,716 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:31,716 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1351771111]
[2025-04-28 21:21:31,716 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1351771111] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:31,716 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [694505354]
[2025-04-28 21:21:31,716 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:31,717 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:31,719 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:31,721 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:31,724 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:31,766 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:31,787 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:31,787 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:31,787 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:31,788 INFO  L256         TraceCheckSpWp]: Trace formula consists of 133 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:31,790 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:31,867 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:31,869 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:32,391 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:32,392 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [694505354] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:32,392 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:32,392 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 13
[2025-04-28 21:21:32,392 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2034030252]
[2025-04-28 21:21:32,392 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,392 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:32,392 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,393 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:32,393 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=32, Invalid=124, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:32,393 INFO  L87              Difference]: Start difference. First operand 71 states and 140 transitions. Second operand  has 13 states, 6 states have (on average 3.0) internal successors, (18), 13 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:32,680 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,680 INFO  L93              Difference]: Finished difference Result 115 states and 225 transitions.
[2025-04-28 21:21:32,681 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:32,681 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 6 states have (on average 3.0) internal successors, (18), 13 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11) Word has length 25
[2025-04-28 21:21:32,681 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,682 INFO  L225             Difference]: With dead ends: 115
[2025-04-28 21:21:32,683 INFO  L226             Difference]: Without dead ends: 106
[2025-04-28 21:21:32,683 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 61 GetRequests, 44 SyntacticMatches, 2 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 31 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=54, Invalid=218, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:32,684 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 14 mSDsluCounter, 181 mSDsCounter, 0 mSdLazyCounter, 221 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 28 SdHoareTripleChecker+Valid, 223 SdHoareTripleChecker+Invalid, 246 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 221 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,684 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [28 Valid, 223 Invalid, 246 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 221 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:32,684 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 106 states.
[2025-04-28 21:21:32,694 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 106 to 82.
[2025-04-28 21:21:32,694 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 35 states have (on average 1.4) internal successors, (49), 47 states have internal predecessors, (49), 18 states have call successors, (18), 6 states have call predecessors, (18), 28 states have return successors, (90), 28 states have call predecessors, (90), 18 states have call successors, (90)
[2025-04-28 21:21:32,695 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 157 transitions.
[2025-04-28 21:21:32,696 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 157 transitions. Word has length 25
[2025-04-28 21:21:32,696 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,696 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 157 transitions.
[2025-04-28 21:21:32,696 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 6 states have (on average 3.0) internal successors, (18), 13 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:32,696 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 157 transitions.
[2025-04-28 21:21:32,698 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:32,698 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,698 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:32,703 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:32,902 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:32,903 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,903 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,903 INFO  L85        PathProgramCache]: Analyzing trace with hash 221647783, now seen corresponding path program 2 times
[2025-04-28 21:21:32,903 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,903 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1213540959]
[2025-04-28 21:21:32,903 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:32,904 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,911 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:32,921 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:32,923 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:32,923 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,031 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:33,031 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,031 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1213540959]
[2025-04-28 21:21:33,031 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1213540959] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,031 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [827652303]
[2025-04-28 21:21:33,031 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:33,031 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,034 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,036 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:33,040 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,081 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 25 statements into 2 equivalence classes.
[2025-04-28 21:21:33,098 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:33,099 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:33,099 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,100 INFO  L256         TraceCheckSpWp]: Trace formula consists of 125 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,101 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,164 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:33,164 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:33,809 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:33,810 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [827652303] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:33,810 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:33,810 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 15
[2025-04-28 21:21:33,810 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1896859185]
[2025-04-28 21:21:33,810 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:33,810 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:33,811 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:33,811 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:33,811 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=173, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:33,811 INFO  L87              Difference]: Start difference. First operand 82 states and 157 transitions. Second operand  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 15 states have internal predecessors, (18), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (12), 6 states have call predecessors, (12), 10 states have call successors, (12)
[2025-04-28 21:21:34,119 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:34,119 INFO  L93              Difference]: Finished difference Result 134 states and 273 transitions.
[2025-04-28 21:21:34,119 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 13 states. 
[2025-04-28 21:21:34,119 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 15 states have internal predecessors, (18), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (12), 6 states have call predecessors, (12), 10 states have call successors, (12) Word has length 25
[2025-04-28 21:21:34,119 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:34,121 INFO  L225             Difference]: With dead ends: 134
[2025-04-28 21:21:34,121 INFO  L226             Difference]: Without dead ends: 132
[2025-04-28 21:21:34,122 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 64 GetRequests, 42 SyntacticMatches, 4 SemanticMatches, 18 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 45 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=80, Invalid=300, Unknown=0, NotChecked=0, Total=380
[2025-04-28 21:21:34,122 INFO  L437           NwaCegarLoop]: 39 mSDtfsCounter, 8 mSDsluCounter, 315 mSDsCounter, 0 mSdLazyCounter, 259 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 354 SdHoareTripleChecker+Invalid, 284 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 259 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:34,122 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 354 Invalid, 284 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 259 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:34,123 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 132 states.
[2025-04-28 21:21:34,135 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 132 to 90.
[2025-04-28 21:21:34,136 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 39 states have (on average 1.358974358974359) internal successors, (53), 51 states have internal predecessors, (53), 18 states have call successors, (18), 6 states have call predecessors, (18), 32 states have return successors, (106), 32 states have call predecessors, (106), 18 states have call successors, (106)
[2025-04-28 21:21:34,137 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 177 transitions.
[2025-04-28 21:21:34,137 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 177 transitions. Word has length 25
[2025-04-28 21:21:34,137 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:34,137 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 177 transitions.
[2025-04-28 21:21:34,137 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.5714285714285716) internal successors, (18), 15 states have internal predecessors, (18), 10 states have call successors, (10), 1 states have call predecessors, (10), 7 states have return successors, (12), 6 states have call predecessors, (12), 10 states have call successors, (12)
[2025-04-28 21:21:34,137 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 177 transitions.
[2025-04-28 21:21:34,142 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:34,142 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,143 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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,148 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:34,343 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,343 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,343 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,344 INFO  L85        PathProgramCache]: Analyzing trace with hash -714230246, now seen corresponding path program 1 times
[2025-04-28 21:21:34,344 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,344 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1448129760]
[2025-04-28 21:21:34,344 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,344 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,348 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:34,352 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:34,352 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,352 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,435 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:34,435 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,435 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1448129760]
[2025-04-28 21:21:34,435 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1448129760] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:34,436 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1483523741]
[2025-04-28 21:21:34,436 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,436 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:34,438 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:34,440 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:34,444 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:34,494 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:34,511 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:34,512 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,512 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,513 INFO  L256         TraceCheckSpWp]: Trace formula consists of 125 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:34,514 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:34,573 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:34,573 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:35,097 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:35,097 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1483523741] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:35,097 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:35,097 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 13
[2025-04-28 21:21:35,098 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1992190086]
[2025-04-28 21:21:35,098 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,098 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:35,098 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,099 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:35,099 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=32, Invalid=124, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:35,099 INFO  L87              Difference]: Start difference. First operand 90 states and 177 transitions. Second operand  has 13 states, 6 states have (on average 3.0) internal successors, (18), 13 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:35,393 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,394 INFO  L93              Difference]: Finished difference Result 124 states and 238 transitions.
[2025-04-28 21:21:35,394 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:35,394 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 6 states have (on average 3.0) internal successors, (18), 13 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11) Word has length 25
[2025-04-28 21:21:35,394 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,396 INFO  L225             Difference]: With dead ends: 124
[2025-04-28 21:21:35,396 INFO  L226             Difference]: Without dead ends: 113
[2025-04-28 21:21:35,396 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 60 GetRequests, 44 SyntacticMatches, 2 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 26 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=53, Invalid=187, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:35,397 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 11 mSDsluCounter, 208 mSDsCounter, 0 mSdLazyCounter, 234 mSolverCounterSat, 27 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 250 SdHoareTripleChecker+Invalid, 261 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 27 IncrementalHoareTripleChecker+Valid, 234 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,397 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 250 Invalid, 261 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [27 Valid, 234 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:35,399 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-04-28 21:21:35,416 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 81.
[2025-04-28 21:21:35,416 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 81 states, 35 states have (on average 1.3714285714285714) internal successors, (48), 46 states have internal predecessors, (48), 17 states have call successors, (17), 6 states have call predecessors, (17), 28 states have return successors, (91), 28 states have call predecessors, (91), 17 states have call successors, (91)
[2025-04-28 21:21:35,417 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 81 states to 81 states and 156 transitions.
[2025-04-28 21:21:35,417 INFO  L79                 Accepts]: Start accepts. Automaton has 81 states and 156 transitions. Word has length 25
[2025-04-28 21:21:35,417 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,418 INFO  L485      AbstractCegarLoop]: Abstraction has 81 states and 156 transitions.
[2025-04-28 21:21:35,418 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 6 states have (on average 3.0) internal successors, (18), 13 states have internal predecessors, (18), 9 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (11), 5 states have call predecessors, (11), 9 states have call successors, (11)
[2025-04-28 21:21:35,418 INFO  L278                IsEmpty]: Start isEmpty. Operand 81 states and 156 transitions.
[2025-04-28 21:21:35,420 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:35,420 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,420 INFO  L218           NwaCegarLoop]: trace histogram [3, 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:35,425 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:35,627 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable14
[2025-04-28 21:21:35,627 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,628 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,628 INFO  L85        PathProgramCache]: Analyzing trace with hash -138906698, now seen corresponding path program 1 times
[2025-04-28 21:21:35,628 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,628 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [300738913]
[2025-04-28 21:21:35,628 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,628 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,632 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:35,635 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:35,636 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,636 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,728 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:35,728 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,728 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [300738913]
[2025-04-28 21:21:35,728 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [300738913] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,728 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:35,728 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:35,729 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1454393917]
[2025-04-28 21:21:35,729 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,729 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:35,729 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,729 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:35,729 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:35,730 INFO  L87              Difference]: Start difference. First operand 81 states and 156 transitions. Second operand  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:35,858 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,858 INFO  L93              Difference]: Finished difference Result 91 states and 176 transitions.
[2025-04-28 21:21:35,860 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:35,861 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6) Word has length 25
[2025-04-28 21:21:35,861 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,862 INFO  L225             Difference]: With dead ends: 91
[2025-04-28 21:21:35,862 INFO  L226             Difference]: Without dead ends: 89
[2025-04-28 21:21:35,862 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=18, Invalid=54, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:35,863 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 4 mSDsluCounter, 204 mSDsCounter, 0 mSdLazyCounter, 140 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 247 SdHoareTripleChecker+Invalid, 143 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 140 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,863 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 247 Invalid, 143 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 140 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:35,863 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 89 states.
[2025-04-28 21:21:35,874 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 89 to 81.
[2025-04-28 21:21:35,874 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 81 states, 35 states have (on average 1.3714285714285714) internal successors, (48), 46 states have internal predecessors, (48), 17 states have call successors, (17), 6 states have call predecessors, (17), 28 states have return successors, (91), 28 states have call predecessors, (91), 17 states have call successors, (91)
[2025-04-28 21:21:35,875 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 81 states to 81 states and 156 transitions.
[2025-04-28 21:21:35,876 INFO  L79                 Accepts]: Start accepts. Automaton has 81 states and 156 transitions. Word has length 25
[2025-04-28 21:21:35,876 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,876 INFO  L485      AbstractCegarLoop]: Abstraction has 81 states and 156 transitions.
[2025-04-28 21:21:35,876 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:35,876 INFO  L278                IsEmpty]: Start isEmpty. Operand 81 states and 156 transitions.
[2025-04-28 21:21:35,877 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:35,877 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,877 INFO  L218           NwaCegarLoop]: trace histogram [3, 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:35,878 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:21:35,878 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,878 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,878 INFO  L85        PathProgramCache]: Analyzing trace with hash -1762104613, now seen corresponding path program 1 times
[2025-04-28 21:21:35,878 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,878 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1517911178]
[2025-04-28 21:21:35,878 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,878 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,891 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:35,893 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:35,894 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,894 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,982 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:35,982 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,982 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1517911178]
[2025-04-28 21:21:35,982 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1517911178] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,982 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:35,982 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:35,982 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1993561087]
[2025-04-28 21:21:35,982 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,983 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:35,983 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,983 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:35,983 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:35,983 INFO  L87              Difference]: Start difference. First operand 81 states and 156 transitions. Second operand  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:36,130 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,130 INFO  L93              Difference]: Finished difference Result 97 states and 191 transitions.
[2025-04-28 21:21:36,133 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:36,133 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6) Word has length 25
[2025-04-28 21:21:36,134 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,135 INFO  L225             Difference]: With dead ends: 97
[2025-04-28 21:21:36,135 INFO  L226             Difference]: Without dead ends: 95
[2025-04-28 21:21:36,135 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=23, Invalid=67, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:36,136 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 5 mSDsluCounter, 179 mSDsCounter, 0 mSdLazyCounter, 141 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 217 SdHoareTripleChecker+Invalid, 143 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 141 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,136 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 217 Invalid, 143 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 141 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:36,137 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 95 states.
[2025-04-28 21:21:36,144 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 95 to 81.
[2025-04-28 21:21:36,144 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 81 states, 35 states have (on average 1.3714285714285714) internal successors, (48), 46 states have internal predecessors, (48), 17 states have call successors, (17), 6 states have call predecessors, (17), 28 states have return successors, (91), 28 states have call predecessors, (91), 17 states have call successors, (91)
[2025-04-28 21:21:36,145 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 81 states to 81 states and 156 transitions.
[2025-04-28 21:21:36,145 INFO  L79                 Accepts]: Start accepts. Automaton has 81 states and 156 transitions. Word has length 25
[2025-04-28 21:21:36,146 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,146 INFO  L485      AbstractCegarLoop]: Abstraction has 81 states and 156 transitions.
[2025-04-28 21:21:36,146 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.2) internal successors, (11), 8 states have internal predecessors, (11), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:36,146 INFO  L278                IsEmpty]: Start isEmpty. Operand 81 states and 156 transitions.
[2025-04-28 21:21:36,147 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:36,147 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,147 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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:36,148 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:21:36,148 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,148 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,148 INFO  L85        PathProgramCache]: Analyzing trace with hash -616949956, now seen corresponding path program 1 times
[2025-04-28 21:21:36,148 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,148 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1958899328]
[2025-04-28 21:21:36,148 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,148 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,152 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:36,156 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:36,156 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,156 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,247 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:36,247 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,247 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1958899328]
[2025-04-28 21:21:36,247 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1958899328] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:36,247 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2058052113]
[2025-04-28 21:21:36,247 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,247 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,250 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:36,252 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:36,255 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:36,306 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:36,325 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:36,325 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,325 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,326 INFO  L256         TraceCheckSpWp]: Trace formula consists of 125 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:36,327 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:36,377 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:36,377 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:37,124 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:37,124 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2058052113] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:37,124 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:37,125 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 9] total 13
[2025-04-28 21:21:37,125 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1852478154]
[2025-04-28 21:21:37,125 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,125 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:37,125 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,126 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:37,126 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=126, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:37,126 INFO  L87              Difference]: Start difference. First operand 81 states and 156 transitions. Second operand  has 13 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 7 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:37,335 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,335 INFO  L93              Difference]: Finished difference Result 135 states and 268 transitions.
[2025-04-28 21:21:37,336 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:37,336 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 7 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 7 states have call successors, (11) Word has length 25
[2025-04-28 21:21:37,336 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,338 INFO  L225             Difference]: With dead ends: 135
[2025-04-28 21:21:37,338 INFO  L226             Difference]: Without dead ends: 129
[2025-04-28 21:21:37,338 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 60 GetRequests, 43 SyntacticMatches, 5 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 21 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=35, Invalid=147, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:37,339 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 6 mSDsluCounter, 217 mSDsCounter, 0 mSdLazyCounter, 193 mSolverCounterSat, 15 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 12 SdHoareTripleChecker+Valid, 251 SdHoareTripleChecker+Invalid, 208 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 15 IncrementalHoareTripleChecker+Valid, 193 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,339 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [12 Valid, 251 Invalid, 208 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [15 Valid, 193 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:37,339 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 129 states.
[2025-04-28 21:21:37,348 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 129 to 77.
[2025-04-28 21:21:37,348 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 77 states, 33 states have (on average 1.393939393939394) internal successors, (46), 44 states have internal predecessors, (46), 17 states have call successors, (17), 6 states have call predecessors, (17), 26 states have return successors, (84), 26 states have call predecessors, (84), 17 states have call successors, (84)
[2025-04-28 21:21:37,349 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 77 states to 77 states and 147 transitions.
[2025-04-28 21:21:37,349 INFO  L79                 Accepts]: Start accepts. Automaton has 77 states and 147 transitions. Word has length 25
[2025-04-28 21:21:37,349 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,350 INFO  L485      AbstractCegarLoop]: Abstraction has 77 states and 147 transitions.
[2025-04-28 21:21:37,350 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 7 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:37,350 INFO  L278                IsEmpty]: Start isEmpty. Operand 77 states and 147 transitions.
[2025-04-28 21:21:37,351 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:37,351 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,351 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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:37,356 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:37,552 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable17
[2025-04-28 21:21:37,552 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,552 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,552 INFO  L85        PathProgramCache]: Analyzing trace with hash -2058146298, now seen corresponding path program 1 times
[2025-04-28 21:21:37,552 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,552 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [758201488]
[2025-04-28 21:21:37,552 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,553 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,556 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:37,561 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:37,561 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,561 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,660 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:37,660 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,660 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [758201488]
[2025-04-28 21:21:37,660 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [758201488] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,660 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [974432571]
[2025-04-28 21:21:37,660 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,660 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,663 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,665 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:37,669 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,726 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:37,744 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:37,744 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,744 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,745 INFO  L256         TraceCheckSpWp]: Trace formula consists of 129 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,748 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:37,896 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:37,896 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:38,663 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:38,663 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [974432571] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:38,664 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:38,664 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 9] total 19
[2025-04-28 21:21:38,664 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1369960321]
[2025-04-28 21:21:38,665 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,665 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:38,666 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,666 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:38,667 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=41, Invalid=301, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:38,667 INFO  L87              Difference]: Start difference. First operand 77 states and 147 transitions. Second operand  has 19 states, 10 states have (on average 2.3) internal successors, (23), 19 states have internal predecessors, (23), 10 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (14), 7 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:21:39,189 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,189 INFO  L93              Difference]: Finished difference Result 169 states and 334 transitions.
[2025-04-28 21:21:39,190 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 24 states. 
[2025-04-28 21:21:39,190 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 10 states have (on average 2.3) internal successors, (23), 19 states have internal predecessors, (23), 10 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (14), 7 states have call predecessors, (14), 10 states have call successors, (14) Word has length 25
[2025-04-28 21:21:39,190 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,192 INFO  L225             Difference]: With dead ends: 169
[2025-04-28 21:21:39,192 INFO  L226             Difference]: Without dead ends: 153
[2025-04-28 21:21:39,193 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 72 GetRequests, 38 SyntacticMatches, 4 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 101 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=124, Invalid=868, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:39,193 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 19 mSDsluCounter, 407 mSDsCounter, 0 mSdLazyCounter, 351 mSolverCounterSat, 74 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 441 SdHoareTripleChecker+Invalid, 425 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 74 IncrementalHoareTripleChecker+Valid, 351 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,193 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 441 Invalid, 425 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [74 Valid, 351 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:39,194 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 153 states.
[2025-04-28 21:21:39,204 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 153 to 79.
[2025-04-28 21:21:39,205 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 34 states have (on average 1.3823529411764706) internal successors, (47), 45 states have internal predecessors, (47), 17 states have call successors, (17), 6 states have call predecessors, (17), 27 states have return successors, (86), 27 states have call predecessors, (86), 17 states have call successors, (86)
[2025-04-28 21:21:39,205 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 150 transitions.
[2025-04-28 21:21:39,206 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 150 transitions. Word has length 25
[2025-04-28 21:21:39,206 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,207 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 150 transitions.
[2025-04-28 21:21:39,207 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 10 states have (on average 2.3) internal successors, (23), 19 states have internal predecessors, (23), 10 states have call successors, (12), 1 states have call predecessors, (12), 9 states have return successors, (14), 7 states have call predecessors, (14), 10 states have call successors, (14)
[2025-04-28 21:21:39,207 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 150 transitions.
[2025-04-28 21:21:39,209 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 26
[2025-04-28 21:21:39,209 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,209 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 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:39,214 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:39,413 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,413 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,413 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,414 INFO  L85        PathProgramCache]: Analyzing trace with hash -1337548127, now seen corresponding path program 1 times
[2025-04-28 21:21:39,414 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,414 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [888019844]
[2025-04-28 21:21:39,414 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,414 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,418 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:39,421 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:39,421 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,421 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,505 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:39,505 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,505 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [888019844]
[2025-04-28 21:21:39,505 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [888019844] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,505 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1428365611]
[2025-04-28 21:21:39,505 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,505 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,508 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,510 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:39,515 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,579 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 25 statements into 1 equivalence classes.
[2025-04-28 21:21:39,596 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 25 of 25 statements.
[2025-04-28 21:21:39,596 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,596 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,597 INFO  L256         TraceCheckSpWp]: Trace formula consists of 125 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:39,598 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,644 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:39,644 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:40,329 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:40,329 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1428365611] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:40,329 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:40,329 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 9] total 13
[2025-04-28 21:21:40,330 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [538176375]
[2025-04-28 21:21:40,330 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,330 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:40,330 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,330 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:40,331 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=126, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:40,331 INFO  L87              Difference]: Start difference. First operand 79 states and 150 transitions. Second operand  has 13 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 7 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:40,521 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,521 INFO  L93              Difference]: Finished difference Result 107 states and 200 transitions.
[2025-04-28 21:21:40,522 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:40,522 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 7 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 7 states have call successors, (11) Word has length 25
[2025-04-28 21:21:40,522 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,523 INFO  L225             Difference]: With dead ends: 107
[2025-04-28 21:21:40,523 INFO  L226             Difference]: Without dead ends: 101
[2025-04-28 21:21:40,523 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 60 GetRequests, 43 SyntacticMatches, 5 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 21 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=35, Invalid=147, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:40,523 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 6 mSDsluCounter, 225 mSDsCounter, 0 mSdLazyCounter, 186 mSolverCounterSat, 17 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 260 SdHoareTripleChecker+Invalid, 203 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 17 IncrementalHoareTripleChecker+Valid, 186 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,524 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 260 Invalid, 203 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [17 Valid, 186 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:40,524 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-04-28 21:21:40,530 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 75.
[2025-04-28 21:21:40,530 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 75 states, 32 states have (on average 1.40625) internal successors, (45), 43 states have internal predecessors, (45), 17 states have call successors, (17), 6 states have call predecessors, (17), 25 states have return successors, (80), 25 states have call predecessors, (80), 17 states have call successors, (80)
[2025-04-28 21:21:40,531 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 75 states to 75 states and 142 transitions.
[2025-04-28 21:21:40,531 INFO  L79                 Accepts]: Start accepts. Automaton has 75 states and 142 transitions. Word has length 25
[2025-04-28 21:21:40,531 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,532 INFO  L485      AbstractCegarLoop]: Abstraction has 75 states and 142 transitions.
[2025-04-28 21:21:40,532 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 7 states have (on average 2.2857142857142856) internal successors, (16), 13 states have internal predecessors, (16), 7 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 7 states have call successors, (11)
[2025-04-28 21:21:40,532 INFO  L278                IsEmpty]: Start isEmpty. Operand 75 states and 142 transitions.
[2025-04-28 21:21:40,533 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:40,533 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,533 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 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:40,538 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:40,737 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19,10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,737 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,738 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,738 INFO  L85        PathProgramCache]: Analyzing trace with hash -1449049876, now seen corresponding path program 1 times
[2025-04-28 21:21:40,738 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,738 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1946439949]
[2025-04-28 21:21:40,738 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,738 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,741 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:40,746 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:40,746 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,746 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,774 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:40,774 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,774 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1946439949]
[2025-04-28 21:21:40,774 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1946439949] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,774 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,774 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:40,775 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [698537082]
[2025-04-28 21:21:40,775 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,775 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:40,775 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,775 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:40,776 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:40,776 INFO  L87              Difference]: Start difference. First operand 75 states and 142 transitions. Second operand  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:40,848 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,848 INFO  L93              Difference]: Finished difference Result 109 states and 215 transitions.
[2025-04-28 21:21:40,849 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:40,849 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 3 states have call successors, (7) Word has length 29
[2025-04-28 21:21:40,849 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,850 INFO  L225             Difference]: With dead ends: 109
[2025-04-28 21:21:40,850 INFO  L226             Difference]: Without dead ends: 109
[2025-04-28 21:21:40,851 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:40,851 INFO  L437           NwaCegarLoop]: 50 mSDtfsCounter, 4 mSDsluCounter, 69 mSDsCounter, 0 mSdLazyCounter, 46 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 119 SdHoareTripleChecker+Invalid, 48 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 46 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,852 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 119 Invalid, 48 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 46 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:40,852 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 109 states.
[2025-04-28 21:21:40,860 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 109 to 93.
[2025-04-28 21:21:40,860 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 93 states, 40 states have (on average 1.4) internal successors, (56), 53 states have internal predecessors, (56), 20 states have call successors, (20), 7 states have call predecessors, (20), 32 states have return successors, (110), 32 states have call predecessors, (110), 20 states have call successors, (110)
[2025-04-28 21:21:40,861 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 93 states to 93 states and 186 transitions.
[2025-04-28 21:21:40,861 INFO  L79                 Accepts]: Start accepts. Automaton has 93 states and 186 transitions. Word has length 29
[2025-04-28 21:21:40,861 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,861 INFO  L485      AbstractCegarLoop]: Abstraction has 93 states and 186 transitions.
[2025-04-28 21:21:40,861 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 4.666666666666667) internal successors, (14), 4 states have internal predecessors, (14), 3 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 3 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:40,862 INFO  L278                IsEmpty]: Start isEmpty. Operand 93 states and 186 transitions.
[2025-04-28 21:21:40,863 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:40,863 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,863 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,863 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20
[2025-04-28 21:21:40,863 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,864 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,864 INFO  L85        PathProgramCache]: Analyzing trace with hash -447237092, now seen corresponding path program 2 times
[2025-04-28 21:21:40,864 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,864 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [485731393]
[2025-04-28 21:21:40,864 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:40,864 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,868 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:40,872 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:40,873 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:40,873 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,951 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:40,951 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,951 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [485731393]
[2025-04-28 21:21:40,951 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [485731393] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,951 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,951 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:40,951 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [799909646]
[2025-04-28 21:21:40,951 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,952 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:40,952 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,952 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:40,952 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:40,952 INFO  L87              Difference]: Start difference. First operand 93 states and 186 transitions. Second operand  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:41,174 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,174 INFO  L93              Difference]: Finished difference Result 117 states and 224 transitions.
[2025-04-28 21:21:41,174 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:41,175 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6) Word has length 29
[2025-04-28 21:21:41,175 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,176 INFO  L225             Difference]: With dead ends: 117
[2025-04-28 21:21:41,176 INFO  L226             Difference]: Without dead ends: 101
[2025-04-28 21:21:41,176 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=100, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:41,177 INFO  L437           NwaCegarLoop]: 39 mSDtfsCounter, 6 mSDsluCounter, 166 mSDsCounter, 0 mSdLazyCounter, 209 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 205 SdHoareTripleChecker+Invalid, 220 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 209 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,177 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 205 Invalid, 220 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 209 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:41,178 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 101 states.
[2025-04-28 21:21:41,184 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 101 to 93.
[2025-04-28 21:21:41,184 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 93 states, 40 states have (on average 1.4) internal successors, (56), 53 states have internal predecessors, (56), 20 states have call successors, (20), 7 states have call predecessors, (20), 32 states have return successors, (99), 32 states have call predecessors, (99), 20 states have call successors, (99)
[2025-04-28 21:21:41,185 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 93 states to 93 states and 175 transitions.
[2025-04-28 21:21:41,185 INFO  L79                 Accepts]: Start accepts. Automaton has 93 states and 175 transitions. Word has length 29
[2025-04-28 21:21:41,185 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,185 INFO  L485      AbstractCegarLoop]: Abstraction has 93 states and 175 transitions.
[2025-04-28 21:21:41,185 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:41,186 INFO  L278                IsEmpty]: Start isEmpty. Operand 93 states and 175 transitions.
[2025-04-28 21:21:41,187 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:41,187 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,187 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,187 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-04-28 21:21:41,187 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,187 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,188 INFO  L85        PathProgramCache]: Analyzing trace with hash -2092507383, now seen corresponding path program 2 times
[2025-04-28 21:21:41,188 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,188 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [713787604]
[2025-04-28 21:21:41,188 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:41,188 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,192 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 29 statements into 2 equivalence classes.
[2025-04-28 21:21:41,196 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:41,196 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:41,196 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,280 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:41,281 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,281 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [713787604]
[2025-04-28 21:21:41,281 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [713787604] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,281 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:41,281 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:41,281 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [849805758]
[2025-04-28 21:21:41,281 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,281 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:41,281 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,282 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:41,282 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:41,282 INFO  L87              Difference]: Start difference. First operand 93 states and 175 transitions. Second operand  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:41,472 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,472 INFO  L93              Difference]: Finished difference Result 117 states and 212 transitions.
[2025-04-28 21:21:41,473 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:41,473 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6) Word has length 29
[2025-04-28 21:21:41,473 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,474 INFO  L225             Difference]: With dead ends: 117
[2025-04-28 21:21:41,475 INFO  L226             Difference]: Without dead ends: 109
[2025-04-28 21:21:41,475 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:41,476 INFO  L437           NwaCegarLoop]: 35 mSDtfsCounter, 7 mSDsluCounter, 149 mSDsCounter, 0 mSdLazyCounter, 190 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 184 SdHoareTripleChecker+Invalid, 199 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 190 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,477 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 184 Invalid, 199 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 190 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:41,477 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 109 states.
[2025-04-28 21:21:41,484 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 109 to 93.
[2025-04-28 21:21:41,484 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 93 states, 40 states have (on average 1.4) internal successors, (56), 53 states have internal predecessors, (56), 20 states have call successors, (20), 7 states have call predecessors, (20), 32 states have return successors, (98), 32 states have call predecessors, (98), 20 states have call successors, (98)
[2025-04-28 21:21:41,485 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 93 states to 93 states and 174 transitions.
[2025-04-28 21:21:41,485 INFO  L79                 Accepts]: Start accepts. Automaton has 93 states and 174 transitions. Word has length 29
[2025-04-28 21:21:41,485 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,486 INFO  L485      AbstractCegarLoop]: Abstraction has 93 states and 174 transitions.
[2025-04-28 21:21:41,486 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.4) internal successors, (12), 8 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:41,486 INFO  L278                IsEmpty]: Start isEmpty. Operand 93 states and 174 transitions.
[2025-04-28 21:21:41,487 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 30
[2025-04-28 21:21:41,487 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,487 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 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:41,487 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable22
[2025-04-28 21:21:41,487 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,488 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,488 INFO  L85        PathProgramCache]: Analyzing trace with hash 1479100894, now seen corresponding path program 1 times
[2025-04-28 21:21:41,488 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,488 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [354276454]
[2025-04-28 21:21:41,488 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,488 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,492 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:41,497 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:41,497 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,497 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,605 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:41,606 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:41,606 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [354276454]
[2025-04-28 21:21:41,606 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [354276454] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:41,606 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [926979333]
[2025-04-28 21:21:41,606 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,606 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,609 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,610 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:41,614 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,687 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 29 statements into 1 equivalence classes.
[2025-04-28 21:21:41,705 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 29 of 29 statements.
[2025-04-28 21:21:41,705 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,705 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,706 INFO  L256         TraceCheckSpWp]: Trace formula consists of 151 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,707 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,787 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:41,787 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:43,670 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:43,671 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [926979333] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,671 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:21:43,671 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [9, 9] total 16
[2025-04-28 21:21:43,671 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [440003905]
[2025-04-28 21:21:43,671 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,671 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:43,671 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,672 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:43,672 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=43, Invalid=197, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:43,672 INFO  L87              Difference]: Start difference. First operand 93 states and 174 transitions. Second operand  has 9 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 9 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:43,817 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,817 INFO  L93              Difference]: Finished difference Result 99 states and 180 transitions.
[2025-04-28 21:21:43,817 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:43,818 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 9 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 4 states have call successors, (7) Word has length 29
[2025-04-28 21:21:43,818 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,819 INFO  L225             Difference]: With dead ends: 99
[2025-04-28 21:21:43,819 INFO  L226             Difference]: Without dead ends: 94
[2025-04-28 21:21:43,821 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 68 GetRequests, 49 SyntacticMatches, 5 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=43, Invalid=197, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:43,822 INFO  L437           NwaCegarLoop]: 34 mSDtfsCounter, 2 mSDsluCounter, 152 mSDsCounter, 0 mSdLazyCounter, 128 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 186 SdHoareTripleChecker+Invalid, 133 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 128 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,825 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 186 Invalid, 133 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 128 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:43,826 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-04-28 21:21:43,832 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 72.
[2025-04-28 21:21:43,832 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 72 states, 30 states have (on average 1.5) internal successors, (45), 42 states have internal predecessors, (45), 19 states have call successors, (19), 7 states have call predecessors, (19), 22 states have return successors, (59), 22 states have call predecessors, (59), 19 states have call successors, (59)
[2025-04-28 21:21:43,833 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 72 states to 72 states and 123 transitions.
[2025-04-28 21:21:43,835 INFO  L79                 Accepts]: Start accepts. Automaton has 72 states and 123 transitions. Word has length 29
[2025-04-28 21:21:43,835 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,835 INFO  L485      AbstractCegarLoop]: Abstraction has 72 states and 123 transitions.
[2025-04-28 21:21:43,835 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.1666666666666665) internal successors, (13), 9 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 5 states have return successors, (7), 5 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:43,835 INFO  L278                IsEmpty]: Start isEmpty. Operand 72 states and 123 transitions.
[2025-04-28 21:21:43,836 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:43,836 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,836 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 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:43,842 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-04-28 21:21:44,037 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,037 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,037 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,037 INFO  L85        PathProgramCache]: Analyzing trace with hash 1978138701, now seen corresponding path program 1 times
[2025-04-28 21:21:44,037 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,038 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [491880007]
[2025-04-28 21:21:44,038 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,038 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,041 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:44,048 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:44,048 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,048 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,157 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:21:44,157 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,157 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [491880007]
[2025-04-28 21:21:44,157 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [491880007] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,157 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,157 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:44,157 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [933381680]
[2025-04-28 21:21:44,157 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,158 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:44,158 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,158 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:44,158 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:44,158 INFO  L87              Difference]: Start difference. First operand 72 states and 123 transitions. Second operand  has 7 states, 5 states have (on average 2.6) internal successors, (13), 7 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:44,305 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,305 INFO  L93              Difference]: Finished difference Result 74 states and 124 transitions.
[2025-04-28 21:21:44,306 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:44,306 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.6) internal successors, (13), 7 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 3 states have call successors, (7) Word has length 33
[2025-04-28 21:21:44,306 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,307 INFO  L225             Difference]: With dead ends: 74
[2025-04-28 21:21:44,307 INFO  L226             Difference]: Without dead ends: 65
[2025-04-28 21:21:44,307 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 5 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:44,308 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 2 mSDsluCounter, 128 mSDsCounter, 0 mSdLazyCounter, 111 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 164 SdHoareTripleChecker+Invalid, 116 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 111 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,308 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 164 Invalid, 116 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 111 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:44,309 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 65 states.
[2025-04-28 21:21:44,312 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 65 to 63.
[2025-04-28 21:21:44,313 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 63 states, 26 states have (on average 1.5384615384615385) internal successors, (40), 37 states have internal predecessors, (40), 18 states have call successors, (18), 7 states have call predecessors, (18), 18 states have return successors, (51), 19 states have call predecessors, (51), 18 states have call successors, (51)
[2025-04-28 21:21:44,313 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 63 states to 63 states and 109 transitions.
[2025-04-28 21:21:44,313 INFO  L79                 Accepts]: Start accepts. Automaton has 63 states and 109 transitions. Word has length 33
[2025-04-28 21:21:44,314 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,314 INFO  L485      AbstractCegarLoop]: Abstraction has 63 states and 109 transitions.
[2025-04-28 21:21:44,314 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.6) internal successors, (13), 7 states have internal predecessors, (13), 3 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 4 states have call predecessors, (7), 3 states have call successors, (7)
[2025-04-28 21:21:44,314 INFO  L278                IsEmpty]: Start isEmpty. Operand 63 states and 109 transitions.
[2025-04-28 21:21:44,315 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:44,315 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,315 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 1, 1, 1, 1, 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:44,315 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable24
[2025-04-28 21:21:44,315 INFO  L403      AbstractCegarLoop]: === Iteration 25 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,316 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,316 INFO  L85        PathProgramCache]: Analyzing trace with hash -1775782918, now seen corresponding path program 1 times
[2025-04-28 21:21:44,316 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,316 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1787512024]
[2025-04-28 21:21:44,316 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,316 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,320 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:44,325 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:44,325 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,326 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,358 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:44,358 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,358 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1787512024]
[2025-04-28 21:21:44,358 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1787512024] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,358 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,358 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:44,358 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [502719643]
[2025-04-28 21:21:44,358 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,359 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:44,359 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,359 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:44,359 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:44,359 INFO  L87              Difference]: Start difference. First operand 63 states and 109 transitions. Second operand  has 4 states, 3 states have (on average 5.0) internal successors, (15), 4 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:44,426 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,426 INFO  L93              Difference]: Finished difference Result 83 states and 143 transitions.
[2025-04-28 21:21:44,427 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:44,427 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 5.0) internal successors, (15), 4 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8) Word has length 33
[2025-04-28 21:21:44,427 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,428 INFO  L225             Difference]: With dead ends: 83
[2025-04-28 21:21:44,428 INFO  L226             Difference]: Without dead ends: 73
[2025-04-28 21:21:44,428 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:44,428 INFO  L437           NwaCegarLoop]: 52 mSDtfsCounter, 4 mSDsluCounter, 72 mSDsCounter, 0 mSdLazyCounter, 48 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 124 SdHoareTripleChecker+Invalid, 50 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 48 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,429 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 124 Invalid, 50 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 48 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:44,429 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 73 states.
[2025-04-28 21:21:44,433 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 73 to 73.
[2025-04-28 21:21:44,433 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 73 states, 31 states have (on average 1.4838709677419355) internal successors, (46), 42 states have internal predecessors, (46), 19 states have call successors, (19), 8 states have call predecessors, (19), 22 states have return successors, (60), 23 states have call predecessors, (60), 19 states have call successors, (60)
[2025-04-28 21:21:44,434 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 73 states to 73 states and 125 transitions.
[2025-04-28 21:21:44,434 INFO  L79                 Accepts]: Start accepts. Automaton has 73 states and 125 transitions. Word has length 33
[2025-04-28 21:21:44,434 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,435 INFO  L485      AbstractCegarLoop]: Abstraction has 73 states and 125 transitions.
[2025-04-28 21:21:44,435 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 5.0) internal successors, (15), 4 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:44,435 INFO  L278                IsEmpty]: Start isEmpty. Operand 73 states and 125 transitions.
[2025-04-28 21:21:44,436 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:44,436 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,436 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 1, 1, 1, 1, 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:44,436 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable25
[2025-04-28 21:21:44,436 INFO  L403      AbstractCegarLoop]: === Iteration 26 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,436 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,436 INFO  L85        PathProgramCache]: Analyzing trace with hash -1935201897, now seen corresponding path program 1 times
[2025-04-28 21:21:44,436 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,437 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [748642034]
[2025-04-28 21:21:44,437 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,437 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,441 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:44,446 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:44,447 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,447 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,474 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 6 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:44,474 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,474 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [748642034]
[2025-04-28 21:21:44,474 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [748642034] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:44,474 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:44,474 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:44,474 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [114212952]
[2025-04-28 21:21:44,475 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,475 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:44,475 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,475 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:44,475 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:44,476 INFO  L87              Difference]: Start difference. First operand 73 states and 125 transitions. Second operand  has 4 states, 3 states have (on average 5.0) internal successors, (15), 4 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:44,531 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:44,532 INFO  L93              Difference]: Finished difference Result 75 states and 121 transitions.
[2025-04-28 21:21:44,532 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 5 states. 
[2025-04-28 21:21:44,532 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 5.0) internal successors, (15), 4 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8) Word has length 33
[2025-04-28 21:21:44,532 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:44,533 INFO  L225             Difference]: With dead ends: 75
[2025-04-28 21:21:44,533 INFO  L226             Difference]: Without dead ends: 70
[2025-04-28 21:21:44,533 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=11, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:44,534 INFO  L437           NwaCegarLoop]: 49 mSDtfsCounter, 3 mSDsluCounter, 70 mSDsCounter, 0 mSdLazyCounter, 38 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 119 SdHoareTripleChecker+Invalid, 40 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 38 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:44,534 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 119 Invalid, 40 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 38 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:44,535 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-04-28 21:21:44,538 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 68.
[2025-04-28 21:21:44,538 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 68 states, 29 states have (on average 1.4827586206896552) internal successors, (43), 39 states have internal predecessors, (43), 18 states have call successors, (18), 8 states have call predecessors, (18), 20 states have return successors, (51), 21 states have call predecessors, (51), 18 states have call successors, (51)
[2025-04-28 21:21:44,539 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 68 states to 68 states and 112 transitions.
[2025-04-28 21:21:44,539 INFO  L79                 Accepts]: Start accepts. Automaton has 68 states and 112 transitions. Word has length 33
[2025-04-28 21:21:44,539 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:44,539 INFO  L485      AbstractCegarLoop]: Abstraction has 68 states and 112 transitions.
[2025-04-28 21:21:44,540 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 5.0) internal successors, (15), 4 states have internal predecessors, (15), 3 states have call successors, (8), 1 states have call predecessors, (8), 3 states have return successors, (8), 3 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:21:44,540 INFO  L278                IsEmpty]: Start isEmpty. Operand 68 states and 112 transitions.
[2025-04-28 21:21:44,540 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:44,541 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:44,541 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 1, 1, 1, 1, 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:44,541 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable26
[2025-04-28 21:21:44,541 INFO  L403      AbstractCegarLoop]: === Iteration 27 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:44,541 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:44,541 INFO  L85        PathProgramCache]: Analyzing trace with hash 1496003927, now seen corresponding path program 2 times
[2025-04-28 21:21:44,541 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:44,542 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [996456415]
[2025-04-28 21:21:44,542 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:44,542 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:44,546 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 33 statements into 2 equivalence classes.
[2025-04-28 21:21:44,557 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:44,565 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:44,565 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,295 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:45,296 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,296 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [996456415]
[2025-04-28 21:21:45,296 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [996456415] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,296 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [817637710]
[2025-04-28 21:21:45,296 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:45,297 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,299 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,301 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:45,304 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,399 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 33 statements into 2 equivalence classes.
[2025-04-28 21:21:45,428 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:45,428 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:45,428 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,433 INFO  L256         TraceCheckSpWp]: Trace formula consists of 181 conjuncts, 85 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,436 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,179 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:46,180 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,925 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:50,925 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [817637710] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,925 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,925 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [14, 14, 14] total 30
[2025-04-28 21:21:50,925 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [987982257]
[2025-04-28 21:21:50,925 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,926 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 30 states
[2025-04-28 21:21:50,926 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,926 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 30 interpolants.
[2025-04-28 21:21:50,926 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=80, Invalid=790, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:50,927 INFO  L87              Difference]: Start difference. First operand 68 states and 112 transitions. Second operand  has 30 states, 15 states have (on average 2.2) internal successors, (33), 30 states have internal predecessors, (33), 16 states have call successors, (17), 1 states have call predecessors, (17), 14 states have return successors, (21), 14 states have call predecessors, (21), 16 states have call successors, (21)
[2025-04-28 21:21:53,051 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,051 INFO  L93              Difference]: Finished difference Result 127 states and 211 transitions.
[2025-04-28 21:21:53,052 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 26 states. 
[2025-04-28 21:21:53,052 INFO  L79                 Accepts]: Start accepts. Automaton has  has 30 states, 15 states have (on average 2.2) internal successors, (33), 30 states have internal predecessors, (33), 16 states have call successors, (17), 1 states have call predecessors, (17), 14 states have return successors, (21), 14 states have call predecessors, (21), 16 states have call successors, (21) Word has length 33
[2025-04-28 21:21:53,052 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,053 INFO  L225             Difference]: With dead ends: 127
[2025-04-28 21:21:53,053 INFO  L226             Difference]: Without dead ends: 112
[2025-04-28 21:21:53,054 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 95 GetRequests, 51 SyntacticMatches, 1 SemanticMatches, 43 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 329 ImplicationChecksByTransitivity, 2.0s TimeCoverageRelationStatistics Valid=193, Invalid=1787, Unknown=0, NotChecked=0, Total=1980
[2025-04-28 21:21:53,058 INFO  L437           NwaCegarLoop]: 46 mSDtfsCounter, 25 mSDsluCounter, 589 mSDsCounter, 0 mSdLazyCounter, 998 mSolverCounterSat, 33 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 43 SdHoareTripleChecker+Valid, 635 SdHoareTripleChecker+Invalid, 1031 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 33 IncrementalHoareTripleChecker+Valid, 998 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,058 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [43 Valid, 635 Invalid, 1031 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [33 Valid, 998 Invalid, 0 Unknown, 0 Unchecked, 1.2s Time]
[2025-04-28 21:21:53,058 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-04-28 21:21:53,067 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 82.
[2025-04-28 21:21:53,067 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 36 states have (on average 1.3888888888888888) internal successors, (50), 46 states have internal predecessors, (50), 19 states have call successors, (19), 9 states have call predecessors, (19), 26 states have return successors, (66), 26 states have call predecessors, (66), 19 states have call successors, (66)
[2025-04-28 21:21:53,068 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 135 transitions.
[2025-04-28 21:21:53,068 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 135 transitions. Word has length 33
[2025-04-28 21:21:53,068 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,068 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 135 transitions.
[2025-04-28 21:21:53,069 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 30 states, 15 states have (on average 2.2) internal successors, (33), 30 states have internal predecessors, (33), 16 states have call successors, (17), 1 states have call predecessors, (17), 14 states have return successors, (21), 14 states have call predecessors, (21), 16 states have call successors, (21)
[2025-04-28 21:21:53,069 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 135 transitions.
[2025-04-28 21:21:53,069 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:53,070 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,070 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 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:53,076 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Ended with exit code 0
[2025-04-28 21:21:53,270 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable27
[2025-04-28 21:21:53,270 INFO  L403      AbstractCegarLoop]: === Iteration 28 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,271 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,271 INFO  L85        PathProgramCache]: Analyzing trace with hash 1141826218, now seen corresponding path program 1 times
[2025-04-28 21:21:53,271 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,271 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1272407684]
[2025-04-28 21:21:53,271 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,271 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,275 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:53,284 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:53,284 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,284 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,427 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:53,427 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:53,428 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1272407684]
[2025-04-28 21:21:53,428 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1272407684] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:53,428 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [446686667]
[2025-04-28 21:21:53,428 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,428 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,430 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:53,432 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:53,435 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-04-28 21:21:53,556 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 33 statements into 1 equivalence classes.
[2025-04-28 21:21:53,581 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:53,581 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,581 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,582 INFO  L256         TraceCheckSpWp]: Trace formula consists of 185 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,584 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,660 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:53,660 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
