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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:14,564 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:14,658 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2f06f3dd-38a3-4684-9f72-b54d7cc324f2/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:14,664 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:14,664 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:14,706 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:14,706 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:14,707 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:14,707 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:14,707 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:14,707 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:14,707 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:14,708 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:14,708 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:14,710 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:14,711 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:14,711 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:14,711 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:14,712 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:14,712 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:14,712 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:14,712 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:14,712 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:14,712 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:14,712 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:14,713 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:14,714 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:15,049 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:15,063 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:15,066 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:15,069 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:15,069 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:15,072 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2f06f3dd-38a3-4684-9f72-b54d7cc324f2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-098.smt2
[2025-04-28 21:21:15,075 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:15,079 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:15,388 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2f06f3dd-38a3-4684-9f72-b54d7cc324f2/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-098.smt2
[2025-04-28 21:21:15,393 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:15,396 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:15,398 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:15,398 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:15,398 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:15,404 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,444 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15 Unit
[2025-04-28 21:21:15,445 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:15,447 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,448 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:15,448 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:15,465 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,466 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,499 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,499 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,503 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,504 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,506 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,508 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,508 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,527 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:15,531 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:15,531 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:15,531 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:15,532 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (1/1) ...
[2025-04-28 21:21:15,535 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:15,550 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:15,562 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:15,566 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:15,582 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:15,582 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:15,583 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:15,583 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:15,583 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:15,583 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:15,583 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:15,583 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:15,583 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:15,583 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_2 given in one single declaration
[2025-04-28 21:21:15,583 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_2
[2025-04-28 21:21:15,583 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_2
[2025-04-28 21:21:15,583 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:15,584 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:15,584 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:15,642 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:15,646 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:15,975 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:15,975 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:15,994 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:15,997 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:15,998 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:15 BoogieIcfgContainer
[2025-04-28 21:21:15,998 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:16,001 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:16,002 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:16,006 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:16,007 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:15" (1/3) ...
[2025-04-28 21:21:16,009 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2154742b and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:16, skipping insertion in model container
[2025-04-28 21:21:16,010 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:15" (2/3) ...
[2025-04-28 21:21:16,011 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@2154742b and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:16, skipping insertion in model container
[2025-04-28 21:21:16,011 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:15" (3/3) ...
[2025-04-28 21:21:16,013 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:16,028 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:16,032 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 5 procedures, 30 locations, 66 edges, 5 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:16,091 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:16,116 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;@5d556c31, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:16,116 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:16,123 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 30 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 21 states have internal predecessors, (21), 15 states have call successors, (15), 4 states have call predecessors, (15), 4 states have return successors, (15), 5 states have call predecessors, (15), 15 states have call successors, (15)
[2025-04-28 21:21:16,141 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:16,141 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,142 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,143 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,150 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,150 INFO  L85        PathProgramCache]: Analyzing trace with hash 467483588, now seen corresponding path program 1 times
[2025-04-28 21:21:16,161 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,161 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [435856279]
[2025-04-28 21:21:16,162 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,163 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,200 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:16,225 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:16,225 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,226 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,466 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:16,467 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,467 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [435856279]
[2025-04-28 21:21:16,468 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [435856279] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,468 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,472 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:16,474 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [857861736]
[2025-04-28 21:21:16,478 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,484 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:16,484 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,515 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:16,516 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:16,520 INFO  L87              Difference]: Start difference. First operand  has 30 states, 9 states have (on average 2.3333333333333335) internal successors, (21), 21 states have internal predecessors, (21), 15 states have call successors, (15), 4 states have call predecessors, (15), 4 states have return successors, (15), 5 states have call predecessors, (15), 15 states have call successors, (15) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:16,640 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,640 INFO  L93              Difference]: Finished difference Result 34 states and 58 transitions.
[2025-04-28 21:21:16,642 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:16,644 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:16,644 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,654 INFO  L225             Difference]: With dead ends: 34
[2025-04-28 21:21:16,654 INFO  L226             Difference]: Without dead ends: 34
[2025-04-28 21:21:16,658 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:16,663 INFO  L437           NwaCegarLoop]: 50 mSDtfsCounter, 2 mSDsluCounter, 83 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 133 SdHoareTripleChecker+Invalid, 23 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,667 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 133 Invalid, 23 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:16,689 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 34 states.
[2025-04-28 21:21:16,716 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 34 to 32.
[2025-04-28 21:21:16,717 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 32 states, 10 states have (on average 2.2) internal successors, (22), 21 states have internal predecessors, (22), 16 states have call successors, (16), 5 states have call predecessors, (16), 5 states have return successors, (18), 6 states have call predecessors, (18), 16 states have call successors, (18)
[2025-04-28 21:21:16,747 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 32 states to 32 states and 56 transitions.
[2025-04-28 21:21:16,753 INFO  L79                 Accepts]: Start accepts. Automaton has 32 states and 56 transitions. Word has length 12
[2025-04-28 21:21:16,754 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,754 INFO  L485      AbstractCegarLoop]: Abstraction has 32 states and 56 transitions.
[2025-04-28 21:21:16,754 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:16,754 INFO  L278                IsEmpty]: Start isEmpty. Operand 32 states and 56 transitions.
[2025-04-28 21:21:16,756 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:16,757 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,757 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,757 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:16,757 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,758 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,758 INFO  L85        PathProgramCache]: Analyzing trace with hash 1693737853, now seen corresponding path program 1 times
[2025-04-28 21:21:16,758 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,758 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1061644015]
[2025-04-28 21:21:16,758 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,759 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,763 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:16,774 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:16,774 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,774 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,889 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:16,889 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,890 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1061644015]
[2025-04-28 21:21:16,890 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1061644015] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,890 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,890 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:16,890 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [844753026]
[2025-04-28 21:21:16,890 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,892 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:16,892 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,893 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:16,893 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:16,893 INFO  L87              Difference]: Start difference. First operand 32 states and 56 transitions. Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:17,019 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,019 INFO  L93              Difference]: Finished difference Result 40 states and 64 transitions.
[2025-04-28 21:21:17,020 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:17,020 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:17,021 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,022 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:21:17,022 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:21:17,022 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,023 INFO  L437           NwaCegarLoop]: 47 mSDtfsCounter, 2 mSDsluCounter, 79 mSDsCounter, 0 mSdLazyCounter, 20 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 126 SdHoareTripleChecker+Invalid, 23 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 20 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,024 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 126 Invalid, 23 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 20 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:17,025 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:21:17,039 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 36.
[2025-04-28 21:21:17,039 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 12 states have (on average 2.0833333333333335) internal successors, (25), 23 states have internal predecessors, (25), 17 states have call successors, (17), 6 states have call predecessors, (17), 6 states have return successors, (17), 7 states have call predecessors, (17), 17 states have call successors, (17)
[2025-04-28 21:21:17,041 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 59 transitions.
[2025-04-28 21:21:17,043 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 59 transitions. Word has length 12
[2025-04-28 21:21:17,043 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,044 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 59 transitions.
[2025-04-28 21:21:17,044 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:17,044 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 59 transitions.
[2025-04-28 21:21:17,046 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:17,049 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,049 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,049 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:17,050 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,050 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,051 INFO  L85        PathProgramCache]: Analyzing trace with hash 712734441, now seen corresponding path program 1 times
[2025-04-28 21:21:17,052 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,052 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1108423335]
[2025-04-28 21:21:17,052 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,052 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,061 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:17,070 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:17,070 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,070 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,119 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:17,119 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,119 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1108423335]
[2025-04-28 21:21:17,119 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1108423335] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,119 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,119 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:17,123 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2145506803]
[2025-04-28 21:21:17,123 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,124 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:17,124 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,124 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:17,125 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,125 INFO  L87              Difference]: Start difference. First operand 36 states and 59 transitions. Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:17,157 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,157 INFO  L93              Difference]: Finished difference Result 40 states and 63 transitions.
[2025-04-28 21:21:17,158 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:17,159 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:17,159 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,160 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:21:17,160 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:21:17,160 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,162 INFO  L437           NwaCegarLoop]: 50 mSDtfsCounter, 1 mSDsluCounter, 91 mSDsCounter, 0 mSdLazyCounter, 8 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 141 SdHoareTripleChecker+Invalid, 8 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 8 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,162 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 141 Invalid, 8 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 8 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:17,163 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:21:17,172 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 38.
[2025-04-28 21:21:17,172 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 38 states, 13 states have (on average 2.0) internal successors, (26), 24 states have internal predecessors, (26), 17 states have call successors, (17), 6 states have call predecessors, (17), 7 states have return successors, (18), 7 states have call predecessors, (18), 17 states have call successors, (18)
[2025-04-28 21:21:17,174 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 38 states to 38 states and 61 transitions.
[2025-04-28 21:21:17,174 INFO  L79                 Accepts]: Start accepts. Automaton has 38 states and 61 transitions. Word has length 12
[2025-04-28 21:21:17,174 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,174 INFO  L485      AbstractCegarLoop]: Abstraction has 38 states and 61 transitions.
[2025-04-28 21:21:17,174 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:17,175 INFO  L278                IsEmpty]: Start isEmpty. Operand 38 states and 61 transitions.
[2025-04-28 21:21:17,176 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:17,176 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,176 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,177 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:17,177 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,177 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,178 INFO  L85        PathProgramCache]: Analyzing trace with hash -1896056821, now seen corresponding path program 1 times
[2025-04-28 21:21:17,178 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,178 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1271418038]
[2025-04-28 21:21:17,178 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,178 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,188 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:17,205 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:17,205 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,205 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,314 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:17,314 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,314 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1271418038]
[2025-04-28 21:21:17,315 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1271418038] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,315 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,315 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:17,315 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1369780692]
[2025-04-28 21:21:17,315 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,315 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:17,315 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,316 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:17,316 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,316 INFO  L87              Difference]: Start difference. First operand 38 states and 61 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:17,456 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,456 INFO  L93              Difference]: Finished difference Result 42 states and 74 transitions.
[2025-04-28 21:21:17,457 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:17,457 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:17,458 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,459 INFO  L225             Difference]: With dead ends: 42
[2025-04-28 21:21:17,459 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:21:17,459 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,460 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 1 mSDsluCounter, 63 mSDsCounter, 0 mSdLazyCounter, 40 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 3 SdHoareTripleChecker+Valid, 106 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 40 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,461 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [3 Valid, 106 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 40 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:17,462 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:21:17,470 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 40.
[2025-04-28 21:21:17,471 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 14 states have (on average 1.9285714285714286) internal successors, (27), 25 states have internal predecessors, (27), 17 states have call successors, (17), 6 states have call predecessors, (17), 8 states have return successors, (28), 8 states have call predecessors, (28), 17 states have call successors, (28)
[2025-04-28 21:21:17,472 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 72 transitions.
[2025-04-28 21:21:17,472 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 72 transitions. Word has length 16
[2025-04-28 21:21:17,472 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,472 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 72 transitions.
[2025-04-28 21:21:17,473 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:17,473 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 72 transitions.
[2025-04-28 21:21:17,474 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:17,474 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,475 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,475 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:17,475 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,475 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,476 INFO  L85        PathProgramCache]: Analyzing trace with hash -505371774, now seen corresponding path program 1 times
[2025-04-28 21:21:17,476 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,476 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1937014851]
[2025-04-28 21:21:17,476 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,476 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,486 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:17,504 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:17,504 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,504 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,570 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:17,571 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,571 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1937014851]
[2025-04-28 21:21:17,571 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1937014851] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,571 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,571 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:17,571 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [999428707]
[2025-04-28 21:21:17,571 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,572 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:17,572 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,572 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:17,572 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,573 INFO  L87              Difference]: Start difference. First operand 40 states and 72 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:17,707 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,709 INFO  L93              Difference]: Finished difference Result 42 states and 73 transitions.
[2025-04-28 21:21:17,710 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:17,710 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:17,710 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,712 INFO  L225             Difference]: With dead ends: 42
[2025-04-28 21:21:17,712 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:21:17,712 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,713 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 1 mSDsluCounter, 58 mSDsCounter, 0 mSdLazyCounter, 33 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 100 SdHoareTripleChecker+Invalid, 38 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 33 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,714 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 100 Invalid, 38 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 33 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:17,715 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:21:17,724 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 40.
[2025-04-28 21:21:17,724 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 14 states have (on average 1.9285714285714286) internal successors, (27), 25 states have internal predecessors, (27), 17 states have call successors, (17), 6 states have call predecessors, (17), 8 states have return successors, (27), 8 states have call predecessors, (27), 17 states have call successors, (27)
[2025-04-28 21:21:17,725 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 71 transitions.
[2025-04-28 21:21:17,726 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 71 transitions. Word has length 16
[2025-04-28 21:21:17,726 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,726 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 71 transitions.
[2025-04-28 21:21:17,726 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:17,726 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 71 transitions.
[2025-04-28 21:21:17,728 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:17,728 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,728 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,729 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:17,729 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,730 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,730 INFO  L85        PathProgramCache]: Analyzing trace with hash 1969881144, now seen corresponding path program 1 times
[2025-04-28 21:21:17,730 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,730 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2007742236]
[2025-04-28 21:21:17,730 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,730 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,736 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:17,742 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:17,742 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,742 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,808 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:17,808 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,809 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2007742236]
[2025-04-28 21:21:17,809 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2007742236] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,809 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,809 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:17,809 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [587104564]
[2025-04-28 21:21:17,809 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,809 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:17,810 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,810 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:17,811 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,811 INFO  L87              Difference]: Start difference. First operand 40 states and 71 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:17,906 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:17,906 INFO  L93              Difference]: Finished difference Result 42 states and 72 transitions.
[2025-04-28 21:21:17,907 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:17,907 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:17,908 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:17,909 INFO  L225             Difference]: With dead ends: 42
[2025-04-28 21:21:17,909 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:21:17,909 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,910 INFO  L437           NwaCegarLoop]: 45 mSDtfsCounter, 1 mSDsluCounter, 65 mSDsCounter, 0 mSdLazyCounter, 34 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 110 SdHoareTripleChecker+Invalid, 36 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 34 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:17,910 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 110 Invalid, 36 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 34 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:17,913 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:21:17,921 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 40.
[2025-04-28 21:21:17,922 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 14 states have (on average 1.9285714285714286) internal successors, (27), 25 states have internal predecessors, (27), 17 states have call successors, (17), 6 states have call predecessors, (17), 8 states have return successors, (26), 8 states have call predecessors, (26), 17 states have call successors, (26)
[2025-04-28 21:21:17,923 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 70 transitions.
[2025-04-28 21:21:17,923 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 70 transitions. Word has length 16
[2025-04-28 21:21:17,923 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:17,923 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 70 transitions.
[2025-04-28 21:21:17,923 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:17,923 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 70 transitions.
[2025-04-28 21:21:17,925 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:17,925 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:17,925 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:17,925 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6
[2025-04-28 21:21:17,925 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:17,926 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:17,926 INFO  L85        PathProgramCache]: Analyzing trace with hash 732254685, now seen corresponding path program 1 times
[2025-04-28 21:21:17,926 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:17,926 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1633592705]
[2025-04-28 21:21:17,926 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:17,927 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:17,932 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:17,937 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:17,937 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:17,937 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:17,988 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:17,988 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:17,988 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1633592705]
[2025-04-28 21:21:17,988 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1633592705] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:17,988 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:17,988 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:17,988 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1721503630]
[2025-04-28 21:21:17,989 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:17,989 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:17,989 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:17,989 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:17,989 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:17,990 INFO  L87              Difference]: Start difference. First operand 40 states and 70 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:18,067 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,067 INFO  L93              Difference]: Finished difference Result 42 states and 71 transitions.
[2025-04-28 21:21:18,069 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:18,069 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:18,069 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,070 INFO  L225             Difference]: With dead ends: 42
[2025-04-28 21:21:18,070 INFO  L226             Difference]: Without dead ends: 42
[2025-04-28 21:21:18,071 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:18,074 INFO  L437           NwaCegarLoop]: 46 mSDtfsCounter, 1 mSDsluCounter, 70 mSDsCounter, 0 mSdLazyCounter, 32 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 116 SdHoareTripleChecker+Invalid, 32 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 32 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,075 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 116 Invalid, 32 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 32 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:18,076 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 42 states.
[2025-04-28 21:21:18,083 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 42 to 40.
[2025-04-28 21:21:18,083 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 14 states have (on average 1.9285714285714286) internal successors, (27), 25 states have internal predecessors, (27), 17 states have call successors, (17), 6 states have call predecessors, (17), 8 states have return successors, (25), 8 states have call predecessors, (25), 17 states have call successors, (25)
[2025-04-28 21:21:18,084 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 69 transitions.
[2025-04-28 21:21:18,084 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 69 transitions. Word has length 16
[2025-04-28 21:21:18,085 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,085 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 69 transitions.
[2025-04-28 21:21:18,088 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 4 states have internal predecessors, (8), 3 states have call successors, (4), 1 states have call predecessors, (4), 3 states have return successors, (4), 2 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:18,088 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 69 transitions.
[2025-04-28 21:21:18,089 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:18,089 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,089 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,089 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:18,090 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,090 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,090 INFO  L85        PathProgramCache]: Analyzing trace with hash 291818315, now seen corresponding path program 1 times
[2025-04-28 21:21:18,090 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,090 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [913265323]
[2025-04-28 21:21:18,090 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,090 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,102 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:18,110 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:18,110 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,110 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,157 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:18,157 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,157 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [913265323]
[2025-04-28 21:21:18,157 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [913265323] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,157 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,157 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:18,158 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [578895003]
[2025-04-28 21:21:18,158 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,158 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:18,158 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,159 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:18,159 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:18,159 INFO  L87              Difference]: Start difference. First operand 40 states and 69 transitions. Second operand  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:18,267 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:18,267 INFO  L93              Difference]: Finished difference Result 40 states and 66 transitions.
[2025-04-28 21:21:18,267 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:18,268 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:18,268 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:18,269 INFO  L225             Difference]: With dead ends: 40
[2025-04-28 21:21:18,269 INFO  L226             Difference]: Without dead ends: 40
[2025-04-28 21:21:18,269 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:18,270 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 1 mSDsluCounter, 63 mSDsCounter, 0 mSdLazyCounter, 41 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 106 SdHoareTripleChecker+Invalid, 41 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 41 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:18,270 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 106 Invalid, 41 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 41 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:18,274 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 40 states.
[2025-04-28 21:21:18,281 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 40 to 40.
[2025-04-28 21:21:18,282 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 40 states, 14 states have (on average 1.9285714285714286) internal successors, (27), 25 states have internal predecessors, (27), 17 states have call successors, (17), 6 states have call predecessors, (17), 8 states have return successors, (22), 8 states have call predecessors, (22), 17 states have call successors, (22)
[2025-04-28 21:21:18,282 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 40 states to 40 states and 66 transitions.
[2025-04-28 21:21:18,283 INFO  L79                 Accepts]: Start accepts. Automaton has 40 states and 66 transitions. Word has length 20
[2025-04-28 21:21:18,285 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:18,286 INFO  L485      AbstractCegarLoop]: Abstraction has 40 states and 66 transitions.
[2025-04-28 21:21:18,286 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 4 states have internal predecessors, (10), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:18,286 INFO  L278                IsEmpty]: Start isEmpty. Operand 40 states and 66 transitions.
[2025-04-28 21:21:18,287 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:18,287 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:18,287 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:18,287 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:18,288 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:18,288 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:18,288 INFO  L85        PathProgramCache]: Analyzing trace with hash 1817016226, now seen corresponding path program 1 times
[2025-04-28 21:21:18,288 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:18,289 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [116705787]
[2025-04-28 21:21:18,289 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:18,289 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:18,306 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:18,326 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:18,326 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:18,326 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:18,680 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:18,683 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:18,683 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [116705787]
[2025-04-28 21:21:18,683 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [116705787] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:18,683 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:18,683 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:18,683 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1295134858]
[2025-04-28 21:21:18,684 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:18,684 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:18,684 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:18,685 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:18,685 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:18,686 INFO  L87              Difference]: Start difference. First operand 40 states and 66 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:19,078 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,078 INFO  L93              Difference]: Finished difference Result 48 states and 96 transitions.
[2025-04-28 21:21:19,079 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:19,079 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:19,079 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,080 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:19,080 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:19,081 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:19,081 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 5 mSDsluCounter, 152 mSDsCounter, 0 mSdLazyCounter, 137 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 195 SdHoareTripleChecker+Invalid, 144 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 137 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,082 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 195 Invalid, 144 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 137 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:19,082 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:19,091 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 44.
[2025-04-28 21:21:19,091 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 44 states, 16 states have (on average 1.8125) internal successors, (29), 27 states have internal predecessors, (29), 17 states have call successors, (17), 6 states have call predecessors, (17), 10 states have return successors, (36), 10 states have call predecessors, (36), 17 states have call successors, (36)
[2025-04-28 21:21:19,094 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 44 states to 44 states and 82 transitions.
[2025-04-28 21:21:19,098 INFO  L79                 Accepts]: Start accepts. Automaton has 44 states and 82 transitions. Word has length 20
[2025-04-28 21:21:19,098 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,098 INFO  L485      AbstractCegarLoop]: Abstraction has 44 states and 82 transitions.
[2025-04-28 21:21:19,098 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:19,098 INFO  L278                IsEmpty]: Start isEmpty. Operand 44 states and 82 transitions.
[2025-04-28 21:21:19,100 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:19,102 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,102 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,102 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:19,102 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,103 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,103 INFO  L85        PathProgramCache]: Analyzing trace with hash 417687460, now seen corresponding path program 1 times
[2025-04-28 21:21:19,103 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,103 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2145711864]
[2025-04-28 21:21:19,104 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,104 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,112 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:19,120 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:19,120 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,120 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:19,386 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:19,387 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:19,387 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2145711864]
[2025-04-28 21:21:19,387 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2145711864] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:19,387 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:19,387 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:19,387 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1633581294]
[2025-04-28 21:21:19,387 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:19,388 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:19,388 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:19,388 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:19,389 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:19,389 INFO  L87              Difference]: Start difference. First operand 44 states and 82 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:19,711 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:19,712 INFO  L93              Difference]: Finished difference Result 48 states and 95 transitions.
[2025-04-28 21:21:19,712 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:19,713 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:19,713 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:19,714 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:19,714 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:19,714 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:19,715 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 5 mSDsluCounter, 157 mSDsCounter, 0 mSdLazyCounter, 137 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 201 SdHoareTripleChecker+Invalid, 144 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 137 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:19,715 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 201 Invalid, 144 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 137 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:19,716 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:19,725 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 44.
[2025-04-28 21:21:19,729 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 44 states, 16 states have (on average 1.8125) internal successors, (29), 27 states have internal predecessors, (29), 17 states have call successors, (17), 6 states have call predecessors, (17), 10 states have return successors, (35), 10 states have call predecessors, (35), 17 states have call successors, (35)
[2025-04-28 21:21:19,731 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 44 states to 44 states and 81 transitions.
[2025-04-28 21:21:19,731 INFO  L79                 Accepts]: Start accepts. Automaton has 44 states and 81 transitions. Word has length 20
[2025-04-28 21:21:19,731 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:19,731 INFO  L485      AbstractCegarLoop]: Abstraction has 44 states and 81 transitions.
[2025-04-28 21:21:19,732 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:19,732 INFO  L278                IsEmpty]: Start isEmpty. Operand 44 states and 81 transitions.
[2025-04-28 21:21:19,734 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:19,734 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:19,734 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:19,734 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:19,735 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:19,736 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:19,736 INFO  L85        PathProgramCache]: Analyzing trace with hash -105653587, now seen corresponding path program 1 times
[2025-04-28 21:21:19,736 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:19,736 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1080513860]
[2025-04-28 21:21:19,736 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:19,736 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:19,747 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:19,755 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:19,755 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:19,755 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,032 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:20,032 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,032 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1080513860]
[2025-04-28 21:21:20,032 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1080513860] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,033 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,033 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:20,033 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [190417592]
[2025-04-28 21:21:20,033 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,033 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:20,033 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,034 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:20,034 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:20,034 INFO  L87              Difference]: Start difference. First operand 44 states and 81 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:20,394 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,394 INFO  L93              Difference]: Finished difference Result 48 states and 94 transitions.
[2025-04-28 21:21:20,395 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:20,395 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:20,395 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,396 INFO  L225             Difference]: With dead ends: 48
[2025-04-28 21:21:20,396 INFO  L226             Difference]: Without dead ends: 48
[2025-04-28 21:21:20,396 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:20,397 INFO  L437           NwaCegarLoop]: 47 mSDtfsCounter, 5 mSDsluCounter, 172 mSDsCounter, 0 mSdLazyCounter, 137 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 219 SdHoareTripleChecker+Invalid, 144 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 137 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,397 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 219 Invalid, 144 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 137 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:20,398 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 48 states.
[2025-04-28 21:21:20,408 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 48 to 44.
[2025-04-28 21:21:20,409 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 44 states, 16 states have (on average 1.8125) internal successors, (29), 27 states have internal predecessors, (29), 17 states have call successors, (17), 6 states have call predecessors, (17), 10 states have return successors, (34), 10 states have call predecessors, (34), 17 states have call successors, (34)
[2025-04-28 21:21:20,410 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 44 states to 44 states and 80 transitions.
[2025-04-28 21:21:20,410 INFO  L79                 Accepts]: Start accepts. Automaton has 44 states and 80 transitions. Word has length 20
[2025-04-28 21:21:20,410 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,410 INFO  L485      AbstractCegarLoop]: Abstraction has 44 states and 80 transitions.
[2025-04-28 21:21:20,411 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:20,411 INFO  L278                IsEmpty]: Start isEmpty. Operand 44 states and 80 transitions.
[2025-04-28 21:21:20,412 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:20,412 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,412 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,413 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:20,413 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,414 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,414 INFO  L85        PathProgramCache]: Analyzing trace with hash 784274678, now seen corresponding path program 1 times
[2025-04-28 21:21:20,415 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,415 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [915661536]
[2025-04-28 21:21:20,415 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,415 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,426 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:20,431 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:20,432 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,432 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:20,635 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:20,635 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:20,635 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [915661536]
[2025-04-28 21:21:20,635 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [915661536] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:20,636 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:20,636 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:20,636 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [737471129]
[2025-04-28 21:21:20,636 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:20,636 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:20,636 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:20,637 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:20,637 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:20,637 INFO  L87              Difference]: Start difference. First operand 44 states and 80 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:20,931 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:20,931 INFO  L93              Difference]: Finished difference Result 50 states and 105 transitions.
[2025-04-28 21:21:20,932 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:20,932 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:20,933 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:20,934 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:21:20,934 INFO  L226             Difference]: Without dead ends: 50
[2025-04-28 21:21:20,934 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:20,935 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 5 mSDsluCounter, 162 mSDsCounter, 0 mSdLazyCounter, 135 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 206 SdHoareTripleChecker+Invalid, 136 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 135 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:20,935 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 206 Invalid, 136 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 135 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:20,936 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-04-28 21:21:20,948 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 46.
[2025-04-28 21:21:20,949 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 17 states have (on average 1.7647058823529411) internal successors, (30), 28 states have internal predecessors, (30), 17 states have call successors, (17), 6 states have call predecessors, (17), 11 states have return successors, (44), 11 states have call predecessors, (44), 17 states have call successors, (44)
[2025-04-28 21:21:20,952 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 91 transitions.
[2025-04-28 21:21:20,952 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 91 transitions. Word has length 20
[2025-04-28 21:21:20,952 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:20,952 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 91 transitions.
[2025-04-28 21:21:20,952 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:20,952 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 91 transitions.
[2025-04-28 21:21:20,955 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:20,955 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:20,956 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:20,956 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12
[2025-04-28 21:21:20,956 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:20,956 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:20,957 INFO  L85        PathProgramCache]: Analyzing trace with hash 260933631, now seen corresponding path program 1 times
[2025-04-28 21:21:20,957 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:20,957 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1189900751]
[2025-04-28 21:21:20,957 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:20,957 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:20,968 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:20,978 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:20,981 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:20,981 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,210 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:21,211 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,211 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1189900751]
[2025-04-28 21:21:21,211 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1189900751] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,211 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,211 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:21,211 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [839752847]
[2025-04-28 21:21:21,211 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,212 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:21,212 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,212 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:21,212 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,213 INFO  L87              Difference]: Start difference. First operand 46 states and 91 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:21,514 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:21,515 INFO  L93              Difference]: Finished difference Result 50 states and 104 transitions.
[2025-04-28 21:21:21,516 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:21,516 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:21,516 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:21,517 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:21:21,518 INFO  L226             Difference]: Without dead ends: 50
[2025-04-28 21:21:21,518 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:21,519 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 5 mSDsluCounter, 162 mSDsCounter, 0 mSdLazyCounter, 135 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 206 SdHoareTripleChecker+Invalid, 136 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 135 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:21,521 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 206 Invalid, 136 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 135 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:21,521 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-04-28 21:21:21,536 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 46.
[2025-04-28 21:21:21,536 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 17 states have (on average 1.7647058823529411) internal successors, (30), 28 states have internal predecessors, (30), 17 states have call successors, (17), 6 states have call predecessors, (17), 11 states have return successors, (43), 11 states have call predecessors, (43), 17 states have call successors, (43)
[2025-04-28 21:21:21,537 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 90 transitions.
[2025-04-28 21:21:21,540 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 90 transitions. Word has length 20
[2025-04-28 21:21:21,540 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:21,540 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 90 transitions.
[2025-04-28 21:21:21,540 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:21,540 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 90 transitions.
[2025-04-28 21:21:21,542 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:21,542 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:21,542 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:21,542 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13
[2025-04-28 21:21:21,542 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:21,543 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:21,543 INFO  L85        PathProgramCache]: Analyzing trace with hash -404467843, now seen corresponding path program 1 times
[2025-04-28 21:21:21,543 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:21,543 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1905205429]
[2025-04-28 21:21:21,543 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:21,543 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:21,550 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:21,557 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:21,557 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:21,558 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:21,786 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:21,787 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:21,787 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1905205429]
[2025-04-28 21:21:21,788 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1905205429] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:21,788 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:21,788 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:21,788 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1216511936]
[2025-04-28 21:21:21,788 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:21,788 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:21,788 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:21,789 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:21,789 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:21,789 INFO  L87              Difference]: Start difference. First operand 46 states and 90 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:22,124 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:22,125 INFO  L93              Difference]: Finished difference Result 50 states and 103 transitions.
[2025-04-28 21:21:22,125 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:22,125 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:22,126 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:22,126 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:21:22,127 INFO  L226             Difference]: Without dead ends: 50
[2025-04-28 21:21:22,127 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:22,128 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 5 mSDsluCounter, 156 mSDsCounter, 0 mSdLazyCounter, 135 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 200 SdHoareTripleChecker+Invalid, 144 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 135 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:22,128 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 200 Invalid, 144 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 135 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:22,128 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-04-28 21:21:22,135 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 46.
[2025-04-28 21:21:22,135 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 17 states have (on average 1.7647058823529411) internal successors, (30), 28 states have internal predecessors, (30), 17 states have call successors, (17), 6 states have call predecessors, (17), 11 states have return successors, (42), 11 states have call predecessors, (42), 17 states have call successors, (42)
[2025-04-28 21:21:22,136 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 89 transitions.
[2025-04-28 21:21:22,136 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 89 transitions. Word has length 20
[2025-04-28 21:21:22,136 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:22,136 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 89 transitions.
[2025-04-28 21:21:22,137 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:22,137 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 89 transitions.
[2025-04-28 21:21:22,138 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:22,138 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,138 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:22,138 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:22,138 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,139 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,139 INFO  L85        PathProgramCache]: Analyzing trace with hash 636273836, now seen corresponding path program 1 times
[2025-04-28 21:21:22,139 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,139 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1964594745]
[2025-04-28 21:21:22,139 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,140 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,145 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:22,151 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:22,151 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,151 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,332 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:22,333 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,333 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1964594745]
[2025-04-28 21:21:22,333 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1964594745] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:22,333 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:22,333 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:22,333 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [229133080]
[2025-04-28 21:21:22,333 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:22,333 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:22,333 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:22,334 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:22,334 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:22,334 INFO  L87              Difference]: Start difference. First operand 46 states and 89 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:22,608 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:22,608 INFO  L93              Difference]: Finished difference Result 50 states and 102 transitions.
[2025-04-28 21:21:22,608 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:22,609 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:22,609 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:22,610 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:21:22,610 INFO  L226             Difference]: Without dead ends: 50
[2025-04-28 21:21:22,612 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:22,613 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 5 mSDsluCounter, 155 mSDsCounter, 0 mSdLazyCounter, 133 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 198 SdHoareTripleChecker+Invalid, 136 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 133 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:22,613 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 198 Invalid, 136 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 133 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:22,613 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-04-28 21:21:22,621 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 46.
[2025-04-28 21:21:22,622 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 17 states have (on average 1.7647058823529411) internal successors, (30), 28 states have internal predecessors, (30), 17 states have call successors, (17), 6 states have call predecessors, (17), 11 states have return successors, (41), 11 states have call predecessors, (41), 17 states have call successors, (41)
[2025-04-28 21:21:22,624 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 88 transitions.
[2025-04-28 21:21:22,624 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 88 transitions. Word has length 20
[2025-04-28 21:21:22,624 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:22,624 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 88 transitions.
[2025-04-28 21:21:22,624 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:22,624 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 88 transitions.
[2025-04-28 21:21:22,625 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:22,626 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:22,626 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:22,626 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable15
[2025-04-28 21:21:22,626 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:22,627 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:22,627 INFO  L85        PathProgramCache]: Analyzing trace with hash -1437209391, now seen corresponding path program 1 times
[2025-04-28 21:21:22,627 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:22,627 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1637160113]
[2025-04-28 21:21:22,627 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:22,627 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:22,635 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:22,641 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:22,641 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:22,642 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:22,840 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:22,840 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:22,840 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1637160113]
[2025-04-28 21:21:22,841 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1637160113] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:22,841 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:22,841 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:22,843 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [571144914]
[2025-04-28 21:21:22,843 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:22,843 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:22,844 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:22,844 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:22,844 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:22,845 INFO  L87              Difference]: Start difference. First operand 46 states and 88 transitions. Second operand  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:23,126 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,127 INFO  L93              Difference]: Finished difference Result 50 states and 101 transitions.
[2025-04-28 21:21:23,127 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:23,128 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5) Word has length 20
[2025-04-28 21:21:23,128 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,129 INFO  L225             Difference]: With dead ends: 50
[2025-04-28 21:21:23,129 INFO  L226             Difference]: Without dead ends: 50
[2025-04-28 21:21:23,129 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 10 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 7 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=21, Invalid=51, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:23,130 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 5 mSDsluCounter, 157 mSDsCounter, 0 mSdLazyCounter, 135 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 11 SdHoareTripleChecker+Valid, 200 SdHoareTripleChecker+Invalid, 136 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 135 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,132 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [11 Valid, 200 Invalid, 136 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 135 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:23,132 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 50 states.
[2025-04-28 21:21:23,139 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 50 to 46.
[2025-04-28 21:21:23,139 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 17 states have (on average 1.7647058823529411) internal successors, (30), 28 states have internal predecessors, (30), 17 states have call successors, (17), 6 states have call predecessors, (17), 11 states have return successors, (40), 11 states have call predecessors, (40), 17 states have call successors, (40)
[2025-04-28 21:21:23,140 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 87 transitions.
[2025-04-28 21:21:23,140 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 87 transitions. Word has length 20
[2025-04-28 21:21:23,140 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,141 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 87 transitions.
[2025-04-28 21:21:23,141 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 4 states have (on average 2.25) internal successors, (9), 6 states have internal predecessors, (9), 4 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 2 states have call predecessors, (5), 4 states have call successors, (5)
[2025-04-28 21:21:23,141 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 87 transitions.
[2025-04-28 21:21:23,142 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:23,142 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,142 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]
[2025-04-28 21:21:23,142 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable16
[2025-04-28 21:21:23,143 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,143 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,143 INFO  L85        PathProgramCache]: Analyzing trace with hash 384874273, now seen corresponding path program 1 times
[2025-04-28 21:21:23,143 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,143 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [56071853]
[2025-04-28 21:21:23,144 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,144 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,155 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:23,162 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:23,162 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,162 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:23,463 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:23,463 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:23,463 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [56071853]
[2025-04-28 21:21:23,463 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [56071853] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:23,463 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:23,463 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:23,464 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [191559264]
[2025-04-28 21:21:23,464 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:23,464 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:23,464 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:23,465 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:23,465 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:23,465 INFO  L87              Difference]: Start difference. First operand 46 states and 87 transitions. Second operand  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:23,915 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:23,915 INFO  L93              Difference]: Finished difference Result 56 states and 135 transitions.
[2025-04-28 21:21:23,916 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:23,916 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6) Word has length 24
[2025-04-28 21:21:23,916 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:23,918 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:23,918 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:23,918 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=34, Invalid=98, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:23,919 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 8 mSDsluCounter, 177 mSDsCounter, 0 mSdLazyCounter, 213 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 220 SdHoareTripleChecker+Invalid, 224 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 213 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:23,919 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 220 Invalid, 224 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 213 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:23,920 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:23,928 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 48.
[2025-04-28 21:21:23,928 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 18 states have (on average 1.7222222222222223) internal successors, (31), 29 states have internal predecessors, (31), 17 states have call successors, (17), 6 states have call predecessors, (17), 12 states have return successors, (50), 12 states have call predecessors, (50), 17 states have call successors, (50)
[2025-04-28 21:21:23,929 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 98 transitions.
[2025-04-28 21:21:23,929 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 98 transitions. Word has length 24
[2025-04-28 21:21:23,930 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:23,930 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 98 transitions.
[2025-04-28 21:21:23,930 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:23,930 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 98 transitions.
[2025-04-28 21:21:23,931 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:23,931 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:23,932 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]
[2025-04-28 21:21:23,932 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable17
[2025-04-28 21:21:23,932 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:23,932 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:23,933 INFO  L85        PathProgramCache]: Analyzing trace with hash 712780141, now seen corresponding path program 1 times
[2025-04-28 21:21:23,933 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:23,933 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1310909894]
[2025-04-28 21:21:23,933 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:23,933 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:23,942 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:23,948 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:23,948 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:23,948 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,053 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:24,053 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:24,053 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1310909894]
[2025-04-28 21:21:24,053 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1310909894] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:24,053 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2021708516]
[2025-04-28 21:21:24,053 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:24,053 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:24,056 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:24,058 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,063 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,113 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:24,135 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:24,135 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:24,135 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:24,138 INFO  L256         TraceCheckSpWp]: Trace formula consists of 129 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:24,148 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:24,256 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:24,257 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:25,171 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:25,171 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2021708516] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:25,171 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:25,172 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 11
[2025-04-28 21:21:25,172 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1847316179]
[2025-04-28 21:21:25,172 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:25,173 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:25,173 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:25,173 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:25,174 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=27, Invalid=83, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:25,174 INFO  L87              Difference]: Start difference. First operand 48 states and 98 transitions. Second operand  has 11 states, 5 states have (on average 3.0) internal successors, (15), 11 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 8 states have call successors, (9)
[2025-04-28 21:21:25,543 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:25,544 INFO  L93              Difference]: Finished difference Result 64 states and 149 transitions.
[2025-04-28 21:21:25,544 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:25,545 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 5 states have (on average 3.0) internal successors, (15), 11 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 8 states have call successors, (9) Word has length 24
[2025-04-28 21:21:25,545 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:25,546 INFO  L225             Difference]: With dead ends: 64
[2025-04-28 21:21:25,548 INFO  L226             Difference]: Without dead ends: 62
[2025-04-28 21:21:25,548 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 42 SyntacticMatches, 5 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=38, Invalid=118, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:25,549 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 6 mSDsluCounter, 186 mSDsCounter, 0 mSdLazyCounter, 210 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 15 SdHoareTripleChecker+Valid, 230 SdHoareTripleChecker+Invalid, 221 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 210 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:25,549 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [15 Valid, 230 Invalid, 221 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 210 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:25,550 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-04-28 21:21:25,564 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 52.
[2025-04-28 21:21:25,566 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 20 states have (on average 1.65) internal successors, (33), 31 states have internal predecessors, (33), 17 states have call successors, (17), 6 states have call predecessors, (17), 14 states have return successors, (66), 14 states have call predecessors, (66), 17 states have call successors, (66)
[2025-04-28 21:21:25,567 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 116 transitions.
[2025-04-28 21:21:25,567 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 116 transitions. Word has length 24
[2025-04-28 21:21:25,567 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:25,568 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 116 transitions.
[2025-04-28 21:21:25,568 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 5 states have (on average 3.0) internal successors, (15), 11 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 8 states have call successors, (9)
[2025-04-28 21:21:25,568 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 116 transitions.
[2025-04-28 21:21:25,570 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:25,571 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:25,571 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]
[2025-04-28 21:21:25,578 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,772 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,772 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:25,772 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:25,772 INFO  L85        PathProgramCache]: Analyzing trace with hash -594186188, now seen corresponding path program 1 times
[2025-04-28 21:21:25,772 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:25,772 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [119264284]
[2025-04-28 21:21:25,773 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,773 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:25,779 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:25,785 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:25,785 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:25,785 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:25,912 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:25,913 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:25,913 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [119264284]
[2025-04-28 21:21:25,913 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [119264284] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:25,913 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [442018928]
[2025-04-28 21:21:25,913 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:25,913 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:25,916 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:25,919 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:25,924 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:25,985 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:26,009 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:26,010 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:26,010 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:26,015 INFO  L256         TraceCheckSpWp]: Trace formula consists of 129 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:26,016 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:26,100 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:26,103 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:26,976 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:26,977 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [442018928] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:26,977 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:26,977 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 11
[2025-04-28 21:21:26,977 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [71113250]
[2025-04-28 21:21:26,977 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:26,978 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:26,978 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:26,978 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:26,979 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=27, Invalid=83, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:26,979 INFO  L87              Difference]: Start difference. First operand 52 states and 116 transitions. Second operand  has 11 states, 5 states have (on average 3.0) internal successors, (15), 11 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 8 states have call successors, (9)
[2025-04-28 21:21:27,272 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:27,272 INFO  L93              Difference]: Finished difference Result 62 states and 145 transitions.
[2025-04-28 21:21:27,273 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:27,273 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 5 states have (on average 3.0) internal successors, (15), 11 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 8 states have call successors, (9) Word has length 24
[2025-04-28 21:21:27,273 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:27,274 INFO  L225             Difference]: With dead ends: 62
[2025-04-28 21:21:27,275 INFO  L226             Difference]: Without dead ends: 60
[2025-04-28 21:21:27,275 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 58 GetRequests, 42 SyntacticMatches, 5 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 18 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=38, Invalid=118, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:27,276 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 7 mSDsluCounter, 161 mSDsCounter, 0 mSdLazyCounter, 160 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 20 SdHoareTripleChecker+Valid, 205 SdHoareTripleChecker+Invalid, 167 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 160 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:27,276 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [20 Valid, 205 Invalid, 167 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 160 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:27,277 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 60 states.
[2025-04-28 21:21:27,286 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 60 to 52.
[2025-04-28 21:21:27,286 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 20 states have (on average 1.65) internal successors, (33), 31 states have internal predecessors, (33), 17 states have call successors, (17), 6 states have call predecessors, (17), 14 states have return successors, (64), 14 states have call predecessors, (64), 17 states have call successors, (64)
[2025-04-28 21:21:27,289 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 114 transitions.
[2025-04-28 21:21:27,289 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 114 transitions. Word has length 24
[2025-04-28 21:21:27,289 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:27,289 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 114 transitions.
[2025-04-28 21:21:27,290 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 5 states have (on average 3.0) internal successors, (15), 11 states have internal predecessors, (15), 8 states have call successors, (9), 1 states have call predecessors, (9), 5 states have return successors, (9), 4 states have call predecessors, (9), 8 states have call successors, (9)
[2025-04-28 21:21:27,290 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 114 transitions.
[2025-04-28 21:21:27,291 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:27,292 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:27,292 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]
[2025-04-28 21:21:27,298 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:27,493 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,493 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:27,494 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:27,494 INFO  L85        PathProgramCache]: Analyzing trace with hash 1203825212, now seen corresponding path program 1 times
[2025-04-28 21:21:27,494 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:27,494 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [179603964]
[2025-04-28 21:21:27,494 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,494 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:27,500 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:27,513 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:27,514 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,514 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,914 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:27,915 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,915 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [179603964]
[2025-04-28 21:21:27,916 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [179603964] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,916 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [380621917]
[2025-04-28 21:21:27,916 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,916 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,919 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,921 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:27,926 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:27,985 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:28,010 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:28,010 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:28,010 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:28,012 INFO  L256         TraceCheckSpWp]: Trace formula consists of 135 conjuncts, 41 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:28,014 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:28,319 INFO  L325             Elim1Store]: treesize reduction 4, result has 50.0 percent of original size
[2025-04-28 21:21:28,320 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 13 treesize of output 10
[2025-04-28 21:21:28,421 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:28,421 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:29,880 INFO  L325             Elim1Store]: treesize reduction 5, result has 37.5 percent of original size
[2025-04-28 21:21:29,881 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 13 treesize of output 9
[2025-04-28 21:21:30,291 INFO  L325             Elim1Store]: treesize reduction 5, result has 37.5 percent of original size
[2025-04-28 21:21:30,291 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 13 treesize of output 9
[2025-04-28 21:21:30,910 INFO  L325             Elim1Store]: treesize reduction 7, result has 12.5 percent of original size
[2025-04-28 21:21:30,910 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 13 treesize of output 1
[2025-04-28 21:21:30,915 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:30,915 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [380621917] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:30,915 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:30,915 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 23
[2025-04-28 21:21:30,917 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1849233587]
[2025-04-28 21:21:30,919 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:30,919 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 23 states
[2025-04-28 21:21:30,919 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:30,920 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 23 interpolants.
[2025-04-28 21:21:30,920 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=443, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:30,920 INFO  L87              Difference]: Start difference. First operand 52 states and 114 transitions. Second operand  has 23 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 22 states have internal predecessors, (26), 12 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (14), 9 states have call predecessors, (14), 12 states have call successors, (14)
[2025-04-28 21:21:32,254 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:32,255 INFO  L93              Difference]: Finished difference Result 86 states and 232 transitions.
[2025-04-28 21:21:32,256 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 19 states. 
[2025-04-28 21:21:32,256 INFO  L79                 Accepts]: Start accepts. Automaton has  has 23 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 22 states have internal predecessors, (26), 12 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (14), 9 states have call predecessors, (14), 12 states have call successors, (14) Word has length 24
[2025-04-28 21:21:32,256 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:32,258 INFO  L225             Difference]: With dead ends: 86
[2025-04-28 21:21:32,258 INFO  L226             Difference]: Without dead ends: 84
[2025-04-28 21:21:32,259 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 68 GetRequests, 36 SyntacticMatches, 0 SemanticMatches, 32 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 141 ImplicationChecksByTransitivity, 0.9s TimeCoverageRelationStatistics Valid=148, Invalid=974, Unknown=0, NotChecked=0, Total=1122
[2025-04-28 21:21:32,260 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 22 mSDsluCounter, 349 mSDsCounter, 0 mSdLazyCounter, 560 mSolverCounterSat, 74 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 26 SdHoareTripleChecker+Valid, 393 SdHoareTripleChecker+Invalid, 634 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 74 IncrementalHoareTripleChecker+Valid, 560 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.9s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:32,260 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [26 Valid, 393 Invalid, 634 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [74 Valid, 560 Invalid, 0 Unknown, 0 Unchecked, 0.9s Time]
[2025-04-28 21:21:32,261 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 84 states.
[2025-04-28 21:21:32,272 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 84 to 66.
[2025-04-28 21:21:32,273 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 66 states, 27 states have (on average 1.4074074074074074) internal successors, (38), 38 states have internal predecessors, (38), 18 states have call successors, (18), 7 states have call predecessors, (18), 20 states have return successors, (109), 20 states have call predecessors, (109), 18 states have call successors, (109)
[2025-04-28 21:21:32,274 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 165 transitions.
[2025-04-28 21:21:32,274 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 165 transitions. Word has length 24
[2025-04-28 21:21:32,274 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:32,274 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 165 transitions.
[2025-04-28 21:21:32,275 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 23 states, 12 states have (on average 2.1666666666666665) internal successors, (26), 22 states have internal predecessors, (26), 12 states have call successors, (13), 1 states have call predecessors, (13), 11 states have return successors, (14), 9 states have call predecessors, (14), 12 states have call successors, (14)
[2025-04-28 21:21:32,275 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 165 transitions.
[2025-04-28 21:21:32,277 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:32,277 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:32,277 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]
[2025-04-28 21:21:32,283 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:32,481 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:32,481 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:32,482 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:32,482 INFO  L85        PathProgramCache]: Analyzing trace with hash 347546545, now seen corresponding path program 1 times
[2025-04-28 21:21:32,482 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:32,482 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1901241315]
[2025-04-28 21:21:32,482 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:32,482 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:32,488 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:32,497 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:32,497 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:32,497 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:32,739 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:32,739 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:32,739 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1901241315]
[2025-04-28 21:21:32,740 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1901241315] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:32,740 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:32,740 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:32,740 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1077734938]
[2025-04-28 21:21:32,740 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:32,740 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:32,740 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:32,741 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:32,741 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:32,741 INFO  L87              Difference]: Start difference. First operand 66 states and 165 transitions. Second operand  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:33,206 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:33,206 INFO  L93              Difference]: Finished difference Result 76 states and 211 transitions.
[2025-04-28 21:21:33,206 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:33,207 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6) Word has length 24
[2025-04-28 21:21:33,207 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:33,209 INFO  L225             Difference]: With dead ends: 76
[2025-04-28 21:21:33,209 INFO  L226             Difference]: Without dead ends: 76
[2025-04-28 21:21:33,209 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=34, Invalid=98, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:33,210 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 8 mSDsluCounter, 175 mSDsCounter, 0 mSdLazyCounter, 211 mSolverCounterSat, 13 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 31 SdHoareTripleChecker+Valid, 218 SdHoareTripleChecker+Invalid, 224 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 13 IncrementalHoareTripleChecker+Valid, 211 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:33,211 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [31 Valid, 218 Invalid, 224 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [13 Valid, 211 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:33,211 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 76 states.
[2025-04-28 21:21:33,230 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 76 to 66.
[2025-04-28 21:21:33,230 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 66 states, 27 states have (on average 1.4074074074074074) internal successors, (38), 38 states have internal predecessors, (38), 18 states have call successors, (18), 7 states have call predecessors, (18), 20 states have return successors, (106), 20 states have call predecessors, (106), 18 states have call successors, (106)
[2025-04-28 21:21:33,231 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 162 transitions.
[2025-04-28 21:21:33,232 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 162 transitions. Word has length 24
[2025-04-28 21:21:33,232 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:33,232 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 162 transitions.
[2025-04-28 21:21:33,232 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:33,232 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 162 transitions.
[2025-04-28 21:21:33,234 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:33,234 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:33,235 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]
[2025-04-28 21:21:33,235 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-04-28 21:21:33,235 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:33,236 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:33,236 INFO  L85        PathProgramCache]: Analyzing trace with hash 629198763, now seen corresponding path program 1 times
[2025-04-28 21:21:33,236 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:33,236 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [956951520]
[2025-04-28 21:21:33,236 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,237 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:33,242 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:33,255 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:33,256 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,256 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,556 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:33,556 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:33,557 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [956951520]
[2025-04-28 21:21:33,557 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [956951520] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:33,557 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [9187037]
[2025-04-28 21:21:33,557 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:33,557 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:33,560 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,562 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:33,566 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:33,631 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:33,654 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:33,654 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:33,655 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:33,656 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:33,658 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:33,699 INFO  L325             Elim1Store]: treesize reduction 4, result has 50.0 percent of original size
[2025-04-28 21:21:33,699 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 17 treesize of output 10
[2025-04-28 21:21:33,797 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:33,797 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:34,504 INFO  L325             Elim1Store]: treesize reduction 5, result has 37.5 percent of original size
[2025-04-28 21:21:34,505 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 17 treesize of output 9
[2025-04-28 21:21:34,653 INFO  L325             Elim1Store]: treesize reduction 5, result has 37.5 percent of original size
[2025-04-28 21:21:34,653 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 17 treesize of output 9
[2025-04-28 21:21:34,794 INFO  L325             Elim1Store]: treesize reduction 7, result has 12.5 percent of original size
[2025-04-28 21:21:34,794 INFO  L354             Elim1Store]: Elim1 eliminated variable of array dimension 1, 0 stores, 2 select indices, 2 select index equivalence classes, 0 disjoint index pairs (out of 1 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 17 treesize of output 1
[2025-04-28 21:21:34,797 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,797 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [9187037] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:34,797 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:34,797 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 8, 8] total 16
[2025-04-28 21:21:34,797 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1911255632]
[2025-04-28 21:21:34,797 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,798 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:34,798 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,798 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:34,799 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=38, Invalid=202, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:34,799 INFO  L87              Difference]: Start difference. First operand 66 states and 162 transitions. Second operand  has 16 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 10 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 6 states have call predecessors, (11), 10 states have call successors, (11)
[2025-04-28 21:21:36,009 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,010 INFO  L93              Difference]: Finished difference Result 117 states and 365 transitions.
[2025-04-28 21:21:36,015 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 23 states. 
[2025-04-28 21:21:36,015 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 10 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 6 states have call predecessors, (11), 10 states have call successors, (11) Word has length 24
[2025-04-28 21:21:36,016 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,018 INFO  L225             Difference]: With dead ends: 117
[2025-04-28 21:21:36,018 INFO  L226             Difference]: Without dead ends: 115
[2025-04-28 21:21:36,019 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 72 GetRequests, 40 SyntacticMatches, 4 SemanticMatches, 28 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 111 ImplicationChecksByTransitivity, 0.6s TimeCoverageRelationStatistics Valid=159, Invalid=711, Unknown=0, NotChecked=0, Total=870
[2025-04-28 21:21:36,021 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 25 mSDsluCounter, 256 mSDsCounter, 0 mSdLazyCounter, 713 mSolverCounterSat, 70 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.7s Time, 0 mProtectedPredicate, 0 mProtectedAction, 41 SdHoareTripleChecker+Valid, 298 SdHoareTripleChecker+Invalid, 783 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 70 IncrementalHoareTripleChecker+Valid, 713 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.8s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,021 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [41 Valid, 298 Invalid, 783 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [70 Valid, 713 Invalid, 0 Unknown, 0 Unchecked, 0.8s Time]
[2025-04-28 21:21:36,021 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 115 states.
[2025-04-28 21:21:36,040 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 115 to 85.
[2025-04-28 21:21:36,041 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 85 states, 35 states have (on average 1.4285714285714286) internal successors, (50), 49 states have internal predecessors, (50), 22 states have call successors, (22), 8 states have call predecessors, (22), 27 states have return successors, (197), 27 states have call predecessors, (197), 22 states have call successors, (197)
[2025-04-28 21:21:36,044 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 85 states to 85 states and 269 transitions.
[2025-04-28 21:21:36,044 INFO  L79                 Accepts]: Start accepts. Automaton has 85 states and 269 transitions. Word has length 24
[2025-04-28 21:21:36,045 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,045 INFO  L485      AbstractCegarLoop]: Abstraction has 85 states and 269 transitions.
[2025-04-28 21:21:36,045 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.625) internal successors, (21), 16 states have internal predecessors, (21), 10 states have call successors, (11), 1 states have call predecessors, (11), 8 states have return successors, (11), 6 states have call predecessors, (11), 10 states have call successors, (11)
[2025-04-28 21:21:36,045 INFO  L278                IsEmpty]: Start isEmpty. Operand 85 states and 269 transitions.
[2025-04-28 21:21:36,047 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:36,047 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,047 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]
[2025-04-28 21:21:36,053 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:36,248 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable22
[2025-04-28 21:21:36,248 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,248 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,249 INFO  L85        PathProgramCache]: Analyzing trace with hash 1467933270, now seen corresponding path program 1 times
[2025-04-28 21:21:36,249 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,249 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [578740753]
[2025-04-28 21:21:36,249 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,249 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,254 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:36,265 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:36,269 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,269 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:36,503 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:36,503 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:36,503 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [578740753]
[2025-04-28 21:21:36,503 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [578740753] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:36,503 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:36,503 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:36,504 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1259347657]
[2025-04-28 21:21:36,504 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:36,504 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:36,504 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:36,504 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:36,505 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:36,505 INFO  L87              Difference]: Start difference. First operand 85 states and 269 transitions. Second operand  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:36,886 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,886 INFO  L93              Difference]: Finished difference Result 99 states and 330 transitions.
[2025-04-28 21:21:36,886 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:36,887 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6) Word has length 24
[2025-04-28 21:21:36,887 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,889 INFO  L225             Difference]: With dead ends: 99
[2025-04-28 21:21:36,889 INFO  L226             Difference]: Without dead ends: 99
[2025-04-28 21:21:36,890 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 14 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=34, Invalid=98, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:36,890 INFO  L437           NwaCegarLoop]: 43 mSDtfsCounter, 8 mSDsluCounter, 177 mSDsCounter, 0 mSdLazyCounter, 213 mSolverCounterSat, 11 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 220 SdHoareTripleChecker+Invalid, 224 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 11 IncrementalHoareTripleChecker+Valid, 213 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,890 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 220 Invalid, 224 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [11 Valid, 213 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:36,891 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 99 states.
[2025-04-28 21:21:36,909 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 99 to 85.
[2025-04-28 21:21:36,909 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 85 states, 35 states have (on average 1.4285714285714286) internal successors, (50), 49 states have internal predecessors, (50), 22 states have call successors, (22), 8 states have call predecessors, (22), 27 states have return successors, (191), 27 states have call predecessors, (191), 22 states have call successors, (191)
[2025-04-28 21:21:36,911 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 85 states to 85 states and 263 transitions.
[2025-04-28 21:21:36,911 INFO  L79                 Accepts]: Start accepts. Automaton has 85 states and 263 transitions. Word has length 24
[2025-04-28 21:21:36,911 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,912 INFO  L485      AbstractCegarLoop]: Abstraction has 85 states and 263 transitions.
[2025-04-28 21:21:36,912 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 4 states have (on average 2.5) internal successors, (10), 7 states have internal predecessors, (10), 5 states have call successors, (6), 1 states have call predecessors, (6), 3 states have return successors, (6), 2 states have call predecessors, (6), 5 states have call successors, (6)
[2025-04-28 21:21:36,912 INFO  L278                IsEmpty]: Start isEmpty. Operand 85 states and 263 transitions.
[2025-04-28 21:21:36,915 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:36,915 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,915 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]
[2025-04-28 21:21:36,915 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable23
[2025-04-28 21:21:36,915 INFO  L403      AbstractCegarLoop]: === Iteration 24 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,916 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,916 INFO  L85        PathProgramCache]: Analyzing trace with hash 526200537, now seen corresponding path program 1 times
[2025-04-28 21:21:36,916 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,916 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [162458354]
[2025-04-28 21:21:36,916 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,916 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,920 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:36,937 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:36,940 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,940 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,316 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 4 refuted. 0 times theorem prover too weak. 2 trivial. 0 not checked.
[2025-04-28 21:21:37,316 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,316 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [162458354]
[2025-04-28 21:21:37,316 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [162458354] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:37,316 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [870723638]
[2025-04-28 21:21:37,317 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,317 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:37,319 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:37,321 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:37,326 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:37,389 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:37,408 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:37,408 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,408 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,409 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:37,411 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
