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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:40,892 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:40,961 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4a819d7e-2d60-49a7-9362-a6bf05dd4d20/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:40,965 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:40,965 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:40,985 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:40,986 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:40,986 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:40,986 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:40,986 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:40,987 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:40,987 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:40,987 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:40,987 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:40,987 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:40,987 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:40,987 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:40,988 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:40,988 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:40,988 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:40,988 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:40,988 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:40,988 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:40,988 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:40,988 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:40,989 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:40,989 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:41,277 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:41,285 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:41,288 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:41,291 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:41,292 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:41,293 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4a819d7e-2d60-49a7-9362-a6bf05dd4d20/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-165.smt2
[2025-04-28 21:21:41,294 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:41,301 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:41,556 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4a819d7e-2d60-49a7-9362-a6bf05dd4d20/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-165.smt2
[2025-04-28 21:21:41,560 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:41,563 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:41,564 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:41,565 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:41,566 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:41,568 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,599 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41 Unit
[2025-04-28 21:21:41,601 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:41,603 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,603 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:41,603 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:41,620 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,620 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,649 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,650 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,653 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,658 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,660 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,661 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,662 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,679 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:41,682 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:41,682 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:41,682 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:41,683 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (1/1) ...
[2025-04-28 21:21:41,686 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:41,703 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:41,717 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:41,721 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:41,738 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:41,739 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:41,739 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:41,739 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure END_QUERY given in one single declaration
[2025-04-28 21:21:41,739 INFO  L130     BoogieDeclarations]: Found specification of procedure END_QUERY
[2025-04-28 21:21:41,739 INFO  L138     BoogieDeclarations]: Found implementation of procedure END_QUERY
[2025-04-28 21:21:41,739 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_3 given in one single declaration
[2025-04-28 21:21:41,739 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_3
[2025-04-28 21:21:41,739 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_3
[2025-04-28 21:21:41,740 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_2 given in one single declaration
[2025-04-28 21:21:41,740 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_2
[2025-04-28 21:21:41,740 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_2
[2025-04-28 21:21:41,740 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_1 given in one single declaration
[2025-04-28 21:21:41,740 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_1
[2025-04-28 21:21:41,740 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_1
[2025-04-28 21:21:41,740 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:41,740 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:41,740 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:41,798 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:41,800 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:41,986 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:41,987 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:42,000 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:42,002 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:42,003 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:42 BoogieIcfgContainer
[2025-04-28 21:21:42,003 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:42,006 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:42,006 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:42,012 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:42,012 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:41" (1/3) ...
[2025-04-28 21:21:42,013 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@230ec6e4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:42, skipping insertion in model container
[2025-04-28 21:21:42,013 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:41" (2/3) ...
[2025-04-28 21:21:42,013 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@230ec6e4 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:42, skipping insertion in model container
[2025-04-28 21:21:42,013 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:42" (3/3) ...
[2025-04-28 21:21:42,014 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:42,031 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:42,036 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 6 procedures, 32 locations, 63 edges, 6 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:42,087 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:42,111 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;@221cc72d, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:42,112 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:42,116 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 32 states, 11 states have (on average 1.9090909090909092) internal successors, (21), 21 states have internal predecessors, (21), 14 states have call successors, (14), 5 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 14 states have call successors, (14)
[2025-04-28 21:21:42,129 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:42,130 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,130 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,131 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,137 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,138 INFO  L85        PathProgramCache]: Analyzing trace with hash 1307935699, now seen corresponding path program 1 times
[2025-04-28 21:21:42,146 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,147 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [360918312]
[2025-04-28 21:21:42,147 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,148 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,190 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:42,222 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:42,223 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,223 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,520 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:42,521 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,522 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [360918312]
[2025-04-28 21:21:42,523 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [360918312] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,527 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:42,530 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:42,531 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1052797771]
[2025-04-28 21:21:42,533 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,538 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:42,541 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,574 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:42,575 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,577 INFO  L87              Difference]: Start difference. First operand  has 32 states, 11 states have (on average 1.9090909090909092) internal successors, (21), 21 states have internal predecessors, (21), 14 states have call successors, (14), 5 states have call predecessors, (14), 5 states have return successors, (14), 6 states have call predecessors, (14), 14 states have call successors, (14) Second operand  has 6 states, 5 states have (on average 2.0) internal successors, (10), 6 states have internal predecessors, (10), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:42,808 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,809 INFO  L93              Difference]: Finished difference Result 36 states and 61 transitions.
[2025-04-28 21:21:42,811 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:42,812 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 5 states have (on average 2.0) internal successors, (10), 6 states have internal predecessors, (10), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5) Word has length 20
[2025-04-28 21:21:42,813 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,820 INFO  L225             Difference]: With dead ends: 36
[2025-04-28 21:21:42,821 INFO  L226             Difference]: Without dead ends: 36
[2025-04-28 21:21:42,823 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 6 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:42,857 INFO  L437           NwaCegarLoop]: 36 mSDtfsCounter, 1 mSDsluCounter, 121 mSDsCounter, 0 mSdLazyCounter, 74 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 157 SdHoareTripleChecker+Invalid, 74 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 74 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,858 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 157 Invalid, 74 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 74 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:42,883 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 36 states.
[2025-04-28 21:21:42,961 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 36 to 36.
[2025-04-28 21:21:42,962 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 36 states, 13 states have (on average 1.6923076923076923) internal successors, (22), 22 states have internal predecessors, (22), 14 states have call successors, (14), 5 states have call predecessors, (14), 8 states have return successors, (25), 8 states have call predecessors, (25), 14 states have call successors, (25)
[2025-04-28 21:21:42,969 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 36 states to 36 states and 61 transitions.
[2025-04-28 21:21:42,971 INFO  L79                 Accepts]: Start accepts. Automaton has 36 states and 61 transitions. Word has length 20
[2025-04-28 21:21:42,973 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,973 INFO  L485      AbstractCegarLoop]: Abstraction has 36 states and 61 transitions.
[2025-04-28 21:21:42,973 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 5 states have (on average 2.0) internal successors, (10), 6 states have internal predecessors, (10), 2 states have call successors, (5), 1 states have call predecessors, (5), 4 states have return successors, (5), 3 states have call predecessors, (5), 2 states have call successors, (5)
[2025-04-28 21:21:42,973 INFO  L278                IsEmpty]: Start isEmpty. Operand 36 states and 61 transitions.
[2025-04-28 21:21:42,976 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:42,977 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,977 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,978 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:42,978 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,980 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,981 INFO  L85        PathProgramCache]: Analyzing trace with hash -1846794398, now seen corresponding path program 1 times
[2025-04-28 21:21:42,981 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,981 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1063173808]
[2025-04-28 21:21:42,981 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,981 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,994 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:43,030 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:43,030 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,030 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,267 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:43,268 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,268 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1063173808]
[2025-04-28 21:21:43,268 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1063173808] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,268 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,268 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:43,268 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1565467941]
[2025-04-28 21:21:43,268 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,270 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:43,270 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,271 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:43,271 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:43,271 INFO  L87              Difference]: Start difference. First operand 36 states and 61 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:43,501 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,501 INFO  L93              Difference]: Finished difference Result 52 states and 101 transitions.
[2025-04-28 21:21:43,503 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:43,503 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6) Word has length 24
[2025-04-28 21:21:43,503 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,505 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:43,505 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:43,506 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:43,509 INFO  L437           NwaCegarLoop]: 46 mSDtfsCounter, 6 mSDsluCounter, 133 mSDsCounter, 0 mSdLazyCounter, 118 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 179 SdHoareTripleChecker+Invalid, 124 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 118 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,509 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 179 Invalid, 124 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 118 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:43,510 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:43,532 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 46.
[2025-04-28 21:21:43,533 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 17 states have (on average 1.7058823529411764) internal successors, (29), 28 states have internal predecessors, (29), 17 states have call successors, (17), 6 states have call predecessors, (17), 11 states have return successors, (38), 11 states have call predecessors, (38), 17 states have call successors, (38)
[2025-04-28 21:21:43,534 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 84 transitions.
[2025-04-28 21:21:43,535 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 84 transitions. Word has length 24
[2025-04-28 21:21:43,535 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,535 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 84 transitions.
[2025-04-28 21:21:43,537 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:43,537 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 84 transitions.
[2025-04-28 21:21:43,540 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:43,540 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,540 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,540 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:43,540 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,541 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,541 INFO  L85        PathProgramCache]: Analyzing trace with hash 1953284504, now seen corresponding path program 1 times
[2025-04-28 21:21:43,543 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,544 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [950871278]
[2025-04-28 21:21:43,544 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,544 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,556 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:43,578 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:43,578 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,578 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,692 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:43,692 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,692 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [950871278]
[2025-04-28 21:21:43,693 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [950871278] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,693 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:43,693 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:43,693 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [708561930]
[2025-04-28 21:21:43,693 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,693 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:43,693 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,694 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:43,694 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:43,694 INFO  L87              Difference]: Start difference. First operand 46 states and 84 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:43,926 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,926 INFO  L93              Difference]: Finished difference Result 54 states and 97 transitions.
[2025-04-28 21:21:43,927 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:43,927 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6) Word has length 24
[2025-04-28 21:21:43,927 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,930 INFO  L225             Difference]: With dead ends: 54
[2025-04-28 21:21:43,930 INFO  L226             Difference]: Without dead ends: 54
[2025-04-28 21:21:43,930 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:43,931 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 6 mSDsluCounter, 130 mSDsCounter, 0 mSdLazyCounter, 115 mSolverCounterSat, 8 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 16 SdHoareTripleChecker+Valid, 174 SdHoareTripleChecker+Invalid, 123 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 8 IncrementalHoareTripleChecker+Valid, 115 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,931 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [16 Valid, 174 Invalid, 123 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [8 Valid, 115 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:43,932 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-04-28 21:21:43,948 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 44.
[2025-04-28 21:21:43,952 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 44 states, 16 states have (on average 1.75) internal successors, (28), 27 states have internal predecessors, (28), 17 states have call successors, (17), 6 states have call predecessors, (17), 10 states have return successors, (32), 10 states have call predecessors, (32), 17 states have call successors, (32)
[2025-04-28 21:21:43,954 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 44 states to 44 states and 77 transitions.
[2025-04-28 21:21:43,957 INFO  L79                 Accepts]: Start accepts. Automaton has 44 states and 77 transitions. Word has length 24
[2025-04-28 21:21:43,957 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,957 INFO  L485      AbstractCegarLoop]: Abstraction has 44 states and 77 transitions.
[2025-04-28 21:21:43,958 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:43,958 INFO  L278                IsEmpty]: Start isEmpty. Operand 44 states and 77 transitions.
[2025-04-28 21:21:43,959 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:43,959 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,959 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,962 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:43,962 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,963 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,963 INFO  L85        PathProgramCache]: Analyzing trace with hash -1127249406, now seen corresponding path program 1 times
[2025-04-28 21:21:43,963 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,963 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [302909188]
[2025-04-28 21:21:43,963 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,963 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,969 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:43,977 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:43,977 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,977 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,110 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:44,110 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,110 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [302909188]
[2025-04-28 21:21:44,110 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [302909188] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:44,110 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1123246471]
[2025-04-28 21:21:44,110 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,110 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,113 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,116 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:44,117 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,158 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:44,179 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:44,179 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,179 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,181 INFO  L256         TraceCheckSpWp]: Trace formula consists of 112 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,187 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,283 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:44,283 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,004 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:45,005 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1123246471] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,005 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,005 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:45,005 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1872173112]
[2025-04-28 21:21:45,005 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,006 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:45,006 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,006 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:45,007 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:45,007 INFO  L87              Difference]: Start difference. First operand 44 states and 77 transitions. Second operand  has 12 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 12 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:45,231 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,231 INFO  L93              Difference]: Finished difference Result 60 states and 113 transitions.
[2025-04-28 21:21:45,231 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:45,232 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 12 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11) Word has length 24
[2025-04-28 21:21:45,232 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,233 INFO  L225             Difference]: With dead ends: 60
[2025-04-28 21:21:45,234 INFO  L226             Difference]: Without dead ends: 58
[2025-04-28 21:21:45,234 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 42 SyntacticMatches, 3 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 15 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:45,235 INFO  L437           NwaCegarLoop]: 41 mSDtfsCounter, 6 mSDsluCounter, 198 mSDsCounter, 0 mSdLazyCounter, 123 mSolverCounterSat, 18 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 239 SdHoareTripleChecker+Invalid, 141 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 18 IncrementalHoareTripleChecker+Valid, 123 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,235 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 239 Invalid, 141 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [18 Valid, 123 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:45,238 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-04-28 21:21:45,254 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 48.
[2025-04-28 21:21:45,257 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 18 states have (on average 1.6666666666666667) internal successors, (30), 29 states have internal predecessors, (30), 17 states have call successors, (17), 6 states have call predecessors, (17), 12 states have return successors, (40), 12 states have call predecessors, (40), 17 states have call successors, (40)
[2025-04-28 21:21:45,259 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 87 transitions.
[2025-04-28 21:21:45,259 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 87 transitions. Word has length 24
[2025-04-28 21:21:45,259 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,259 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 87 transitions.
[2025-04-28 21:21:45,259 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 12 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:45,259 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 87 transitions.
[2025-04-28 21:21:45,264 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:45,264 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,264 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,274 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:45,465 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,465 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,466 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,466 INFO  L85        PathProgramCache]: Analyzing trace with hash 1441521749, now seen corresponding path program 1 times
[2025-04-28 21:21:45,466 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,466 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [585572780]
[2025-04-28 21:21:45,466 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,466 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,473 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:45,491 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:45,491 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,491 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,627 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:45,627 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,627 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [585572780]
[2025-04-28 21:21:45,627 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [585572780] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:45,628 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1202820706]
[2025-04-28 21:21:45,628 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,628 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:45,632 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,634 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:45,639 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:45,684 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:45,707 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:45,708 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,708 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,709 INFO  L256         TraceCheckSpWp]: Trace formula consists of 108 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:45,711 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:45,801 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:45,805 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:46,458 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:46,458 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1202820706] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:46,459 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:46,459 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 12
[2025-04-28 21:21:46,459 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [320382634]
[2025-04-28 21:21:46,459 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:46,459 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 12 states
[2025-04-28 21:21:46,460 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:46,460 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 12 interpolants.
[2025-04-28 21:21:46,461 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=28, Invalid=104, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:46,461 INFO  L87              Difference]: Start difference. First operand 48 states and 87 transitions. Second operand  has 12 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 12 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:46,715 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,715 INFO  L93              Difference]: Finished difference Result 60 states and 110 transitions.
[2025-04-28 21:21:46,718 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:21:46,718 INFO  L79                 Accepts]: Start accepts. Automaton has  has 12 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 12 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11) Word has length 24
[2025-04-28 21:21:46,718 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,752 INFO  L225             Difference]: With dead ends: 60
[2025-04-28 21:21:46,752 INFO  L226             Difference]: Without dead ends: 58
[2025-04-28 21:21:46,752 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 42 SyntacticMatches, 3 SemanticMatches, 11 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 15 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=33, Invalid=123, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:46,753 INFO  L437           NwaCegarLoop]: 41 mSDtfsCounter, 7 mSDsluCounter, 200 mSDsCounter, 0 mSdLazyCounter, 138 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 13 SdHoareTripleChecker+Valid, 241 SdHoareTripleChecker+Invalid, 154 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 138 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,753 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [13 Valid, 241 Invalid, 154 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 138 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:46,755 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-04-28 21:21:46,767 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 46.
[2025-04-28 21:21:46,767 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 17 states have (on average 1.7058823529411764) internal successors, (29), 28 states have internal predecessors, (29), 17 states have call successors, (17), 6 states have call predecessors, (17), 11 states have return successors, (35), 11 states have call predecessors, (35), 17 states have call successors, (35)
[2025-04-28 21:21:46,769 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 81 transitions.
[2025-04-28 21:21:46,769 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 81 transitions. Word has length 24
[2025-04-28 21:21:46,770 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,771 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 81 transitions.
[2025-04-28 21:21:46,771 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 12 states, 6 states have (on average 2.6666666666666665) internal successors, (16), 12 states have internal predecessors, (16), 8 states have call successors, (9), 1 states have call predecessors, (9), 6 states have return successors, (11), 5 states have call predecessors, (11), 8 states have call successors, (11)
[2025-04-28 21:21:46,771 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 81 transitions.
[2025-04-28 21:21:46,773 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:46,774 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,774 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,780 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:46,978 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,978 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,979 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,980 INFO  L85        PathProgramCache]: Analyzing trace with hash 495948509, now seen corresponding path program 1 times
[2025-04-28 21:21:46,980 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,980 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1729454014]
[2025-04-28 21:21:46,980 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,980 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,988 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:47,001 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:47,001 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,001 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,335 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:47,335 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,336 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1729454014]
[2025-04-28 21:21:47,336 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1729454014] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,336 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [783030820]
[2025-04-28 21:21:47,336 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,336 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,340 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,342 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:47,347 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,386 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:47,406 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:47,406 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,406 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,408 INFO  L256         TraceCheckSpWp]: Trace formula consists of 108 conjuncts, 27 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,409 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,596 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:47,596 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,449 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:48,449 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [783030820] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,450 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,450 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 9, 9] total 19
[2025-04-28 21:21:48,450 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [304297454]
[2025-04-28 21:21:48,450 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,450 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:48,450 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,451 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:48,451 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=53, Invalid=289, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:48,452 INFO  L87              Difference]: Start difference. First operand 46 states and 81 transitions. Second operand  has 19 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (13), 7 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:21:48,981 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:48,981 INFO  L93              Difference]: Finished difference Result 68 states and 128 transitions.
[2025-04-28 21:21:48,981 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:48,982 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (13), 7 states have call predecessors, (13), 11 states have call successors, (13) Word has length 24
[2025-04-28 21:21:48,982 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:48,984 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:21:48,984 INFO  L226             Difference]: Without dead ends: 68
[2025-04-28 21:21:48,984 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 61 GetRequests, 40 SyntacticMatches, 0 SemanticMatches, 21 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 60 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=78, Invalid=428, Unknown=0, NotChecked=0, Total=506
[2025-04-28 21:21:48,985 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 8 mSDsluCounter, 332 mSDsCounter, 0 mSdLazyCounter, 361 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 370 SdHoareTripleChecker+Invalid, 386 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 361 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:48,986 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 370 Invalid, 386 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 361 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:48,987 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 68 states.
[2025-04-28 21:21:48,998 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 68 to 48.
[2025-04-28 21:21:48,998 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 48 states, 18 states have (on average 1.6666666666666667) internal successors, (30), 29 states have internal predecessors, (30), 17 states have call successors, (17), 6 states have call predecessors, (17), 12 states have return successors, (39), 12 states have call predecessors, (39), 17 states have call successors, (39)
[2025-04-28 21:21:48,999 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 48 states to 48 states and 86 transitions.
[2025-04-28 21:21:49,000 INFO  L79                 Accepts]: Start accepts. Automaton has 48 states and 86 transitions. Word has length 24
[2025-04-28 21:21:49,000 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,000 INFO  L485      AbstractCegarLoop]: Abstraction has 48 states and 86 transitions.
[2025-04-28 21:21:49,000 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 19 states have internal predecessors, (22), 11 states have call successors, (13), 1 states have call predecessors, (13), 8 states have return successors, (13), 7 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:21:49,000 INFO  L278                IsEmpty]: Start isEmpty. Operand 48 states and 86 transitions.
[2025-04-28 21:21:49,002 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:49,002 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,002 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,008 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:49,206 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:49,206 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,207 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,207 INFO  L85        PathProgramCache]: Analyzing trace with hash -2094238595, now seen corresponding path program 1 times
[2025-04-28 21:21:49,207 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,207 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [839072651]
[2025-04-28 21:21:49,207 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,207 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,213 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:49,218 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:49,220 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,220 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,325 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:49,325 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,325 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [839072651]
[2025-04-28 21:21:49,325 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [839072651] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,325 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,325 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:49,325 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1276975269]
[2025-04-28 21:21:49,325 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,326 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:49,326 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,326 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:49,327 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:49,327 INFO  L87              Difference]: Start difference. First operand 48 states and 86 transitions. Second operand  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:49,452 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,452 INFO  L93              Difference]: Finished difference Result 66 states and 117 transitions.
[2025-04-28 21:21:49,453 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:49,453 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6) Word has length 24
[2025-04-28 21:21:49,453 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,454 INFO  L225             Difference]: With dead ends: 66
[2025-04-28 21:21:49,454 INFO  L226             Difference]: Without dead ends: 62
[2025-04-28 21:21:49,455 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 7 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 5 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=13, Invalid=29, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:49,455 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 3 mSDsluCounter, 126 mSDsCounter, 0 mSdLazyCounter, 76 mSolverCounterSat, 3 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 166 SdHoareTripleChecker+Invalid, 79 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 3 IncrementalHoareTripleChecker+Valid, 76 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,456 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 166 Invalid, 79 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [3 Valid, 76 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:49,456 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 62 states.
[2025-04-28 21:21:49,465 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 62 to 58.
[2025-04-28 21:21:49,466 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 58 states, 23 states have (on average 1.5217391304347827) internal successors, (35), 34 states have internal predecessors, (35), 17 states have call successors, (17), 6 states have call predecessors, (17), 17 states have return successors, (54), 17 states have call predecessors, (54), 17 states have call successors, (54)
[2025-04-28 21:21:49,467 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 106 transitions.
[2025-04-28 21:21:49,467 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 106 transitions. Word has length 24
[2025-04-28 21:21:49,468 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,468 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 106 transitions.
[2025-04-28 21:21:49,468 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 4 states have (on average 3.0) internal successors, (12), 6 states have internal predecessors, (12), 4 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 3 states have call predecessors, (6), 4 states have call successors, (6)
[2025-04-28 21:21:49,468 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 106 transitions.
[2025-04-28 21:21:49,469 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:49,469 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,470 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,470 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7
[2025-04-28 21:21:49,470 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,470 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,470 INFO  L85        PathProgramCache]: Analyzing trace with hash -1063247401, now seen corresponding path program 1 times
[2025-04-28 21:21:49,470 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,471 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [991326782]
[2025-04-28 21:21:49,471 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,471 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,475 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:49,479 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:49,479 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,479 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,580 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:49,580 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,580 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [991326782]
[2025-04-28 21:21:49,581 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [991326782] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,581 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,581 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:49,581 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [31250666]
[2025-04-28 21:21:49,581 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,582 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:49,582 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,582 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:49,582 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:49,583 INFO  L87              Difference]: Start difference. First operand 58 states and 106 transitions. Second operand  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:49,725 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,726 INFO  L93              Difference]: Finished difference Result 66 states and 122 transitions.
[2025-04-28 21:21:49,726 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:49,726 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:49,727 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,728 INFO  L225             Difference]: With dead ends: 66
[2025-04-28 21:21:49,728 INFO  L226             Difference]: Without dead ends: 64
[2025-04-28 21:21:49,728 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:49,729 INFO  L437           NwaCegarLoop]: 46 mSDtfsCounter, 2 mSDsluCounter, 189 mSDsCounter, 0 mSdLazyCounter, 117 mSolverCounterSat, 1 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 235 SdHoareTripleChecker+Invalid, 118 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 1 IncrementalHoareTripleChecker+Valid, 117 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,729 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 235 Invalid, 118 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [1 Valid, 117 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:49,730 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 64 states.
[2025-04-28 21:21:49,739 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 64 to 62.
[2025-04-28 21:21:49,739 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 25 states have (on average 1.48) internal successors, (37), 36 states have internal predecessors, (37), 17 states have call successors, (17), 6 states have call predecessors, (17), 19 states have return successors, (61), 19 states have call predecessors, (61), 17 states have call successors, (61)
[2025-04-28 21:21:49,740 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 115 transitions.
[2025-04-28 21:21:49,741 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 115 transitions. Word has length 24
[2025-04-28 21:21:49,741 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,741 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 115 transitions.
[2025-04-28 21:21:49,741 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:49,741 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 115 transitions.
[2025-04-28 21:21:49,743 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:49,743 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,743 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,743 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8
[2025-04-28 21:21:49,743 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,744 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,744 INFO  L85        PathProgramCache]: Analyzing trace with hash 1790523553, now seen corresponding path program 1 times
[2025-04-28 21:21:49,744 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,744 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [259505291]
[2025-04-28 21:21:49,744 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,744 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,749 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:49,752 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:49,752 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,752 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:49,858 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:49,858 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:49,858 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [259505291]
[2025-04-28 21:21:49,858 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [259505291] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:49,858 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:49,858 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:49,858 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1575103821]
[2025-04-28 21:21:49,859 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,859 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:49,859 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,859 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:49,860 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:49,860 INFO  L87              Difference]: Start difference. First operand 62 states and 115 transitions. Second operand  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:50,013 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,016 INFO  L93              Difference]: Finished difference Result 70 states and 131 transitions.
[2025-04-28 21:21:50,017 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:50,017 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:50,017 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,018 INFO  L225             Difference]: With dead ends: 70
[2025-04-28 21:21:50,018 INFO  L226             Difference]: Without dead ends: 68
[2025-04-28 21:21:50,019 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:50,019 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 3 mSDsluCounter, 165 mSDsCounter, 0 mSdLazyCounter, 99 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 205 SdHoareTripleChecker+Invalid, 99 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 99 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,020 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 205 Invalid, 99 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 99 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:50,023 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 68 states.
[2025-04-28 21:21:50,038 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 68 to 64.
[2025-04-28 21:21:50,038 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 64 states, 26 states have (on average 1.4615384615384615) internal successors, (38), 37 states have internal predecessors, (38), 17 states have call successors, (17), 6 states have call predecessors, (17), 20 states have return successors, (65), 20 states have call predecessors, (65), 17 states have call successors, (65)
[2025-04-28 21:21:50,040 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 64 states to 64 states and 120 transitions.
[2025-04-28 21:21:50,040 INFO  L79                 Accepts]: Start accepts. Automaton has 64 states and 120 transitions. Word has length 24
[2025-04-28 21:21:50,040 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,040 INFO  L485      AbstractCegarLoop]: Abstraction has 64 states and 120 transitions.
[2025-04-28 21:21:50,040 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:50,041 INFO  L278                IsEmpty]: Start isEmpty. Operand 64 states and 120 transitions.
[2025-04-28 21:21:50,042 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:50,042 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,042 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,042 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable9
[2025-04-28 21:21:50,043 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,043 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,043 INFO  L85        PathProgramCache]: Analyzing trace with hash -1783845572, now seen corresponding path program 1 times
[2025-04-28 21:21:50,043 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,043 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1437172650]
[2025-04-28 21:21:50,043 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,044 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,048 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:50,052 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:50,052 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,052 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,141 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:50,142 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,142 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1437172650]
[2025-04-28 21:21:50,142 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1437172650] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,142 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,142 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:50,142 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [366057845]
[2025-04-28 21:21:50,142 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,143 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:50,143 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,143 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:50,144 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:50,144 INFO  L87              Difference]: Start difference. First operand 64 states and 120 transitions. Second operand  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:50,295 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,297 INFO  L93              Difference]: Finished difference Result 74 states and 141 transitions.
[2025-04-28 21:21:50,297 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:50,298 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6) Word has length 24
[2025-04-28 21:21:50,298 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,299 INFO  L225             Difference]: With dead ends: 74
[2025-04-28 21:21:50,300 INFO  L226             Difference]: Without dead ends: 72
[2025-04-28 21:21:50,300 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 9 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:50,301 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 2 mSDsluCounter, 178 mSDsCounter, 0 mSdLazyCounter, 116 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 222 SdHoareTripleChecker+Invalid, 118 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 116 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,302 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 222 Invalid, 118 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 116 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:50,303 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 72 states.
[2025-04-28 21:21:50,315 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 72 to 66.
[2025-04-28 21:21:50,315 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 66 states, 27 states have (on average 1.4444444444444444) internal successors, (39), 38 states have internal predecessors, (39), 17 states have call successors, (17), 6 states have call predecessors, (17), 21 states have return successors, (69), 21 states have call predecessors, (69), 17 states have call successors, (69)
[2025-04-28 21:21:50,316 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 125 transitions.
[2025-04-28 21:21:50,316 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 125 transitions. Word has length 24
[2025-04-28 21:21:50,317 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,317 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 125 transitions.
[2025-04-28 21:21:50,317 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.2) internal successors, (11), 7 states have internal predecessors, (11), 3 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (6), 4 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:50,317 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 125 transitions.
[2025-04-28 21:21:50,321 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:50,321 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,321 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,321 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10
[2025-04-28 21:21:50,321 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,322 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,322 INFO  L85        PathProgramCache]: Analyzing trace with hash 1628754823, now seen corresponding path program 1 times
[2025-04-28 21:21:50,322 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,322 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [426607046]
[2025-04-28 21:21:50,322 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,322 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,329 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:50,338 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:50,338 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,338 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,458 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:50,458 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,459 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [426607046]
[2025-04-28 21:21:50,459 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [426607046] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:50,459 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:50,459 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:50,459 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2009362921]
[2025-04-28 21:21:50,459 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,459 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:50,459 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,460 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:50,460 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:50,461 INFO  L87              Difference]: Start difference. First operand 66 states and 125 transitions. Second operand  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:50,759 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,759 INFO  L93              Difference]: Finished difference Result 90 states and 167 transitions.
[2025-04-28 21:21:50,760 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:50,760 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7) Word has length 28
[2025-04-28 21:21:50,760 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,762 INFO  L225             Difference]: With dead ends: 90
[2025-04-28 21:21:50,762 INFO  L226             Difference]: Without dead ends: 90
[2025-04-28 21:21:50,763 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 13 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 4 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=32, Invalid=100, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:50,764 INFO  L437           NwaCegarLoop]: 41 mSDtfsCounter, 7 mSDsluCounter, 175 mSDsCounter, 0 mSdLazyCounter, 228 mSolverCounterSat, 12 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 216 SdHoareTripleChecker+Invalid, 240 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 12 IncrementalHoareTripleChecker+Valid, 228 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,765 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 216 Invalid, 240 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [12 Valid, 228 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:50,766 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-04-28 21:21:50,784 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 78.
[2025-04-28 21:21:50,785 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 78 states, 33 states have (on average 1.3636363636363635) internal successors, (45), 44 states have internal predecessors, (45), 17 states have call successors, (17), 6 states have call predecessors, (17), 27 states have return successors, (88), 27 states have call predecessors, (88), 17 states have call successors, (88)
[2025-04-28 21:21:50,786 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 78 states to 78 states and 150 transitions.
[2025-04-28 21:21:50,786 INFO  L79                 Accepts]: Start accepts. Automaton has 78 states and 150 transitions. Word has length 28
[2025-04-28 21:21:50,786 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,786 INFO  L485      AbstractCegarLoop]: Abstraction has 78 states and 150 transitions.
[2025-04-28 21:21:50,787 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:50,787 INFO  L278                IsEmpty]: Start isEmpty. Operand 78 states and 150 transitions.
[2025-04-28 21:21:50,788 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:50,789 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,789 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,789 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable11
[2025-04-28 21:21:50,789 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,789 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,790 INFO  L85        PathProgramCache]: Analyzing trace with hash -1233312025, now seen corresponding path program 2 times
[2025-04-28 21:21:50,790 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,790 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1925485033]
[2025-04-28 21:21:50,790 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:50,790 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,798 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:50,808 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:50,810 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:50,810 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,953 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:50,953 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,954 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1925485033]
[2025-04-28 21:21:50,954 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1925485033] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,954 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1222377242]
[2025-04-28 21:21:50,954 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:50,954 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,957 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,959 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:50,965 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:51,015 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 28 statements into 2 equivalence classes.
[2025-04-28 21:21:51,038 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:51,038 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:51,039 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,040 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:51,042 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:51,116 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:51,116 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:52,013 INFO  L134       CoverageAnalysis]: Checked inductivity of 10 backedges. 2 proven. 5 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:52,014 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1222377242] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:52,014 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:52,014 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 10, 10] total 15
[2025-04-28 21:21:52,014 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [803878949]
[2025-04-28 21:21:52,014 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:52,014 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:52,014 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:52,015 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:52,015 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=37, Invalid=173, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:52,016 INFO  L87              Difference]: Start difference. First operand 78 states and 150 transitions. Second operand  has 15 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 15 states have internal predecessors, (19), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (13), 6 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:52,281 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:52,281 INFO  L93              Difference]: Finished difference Result 112 states and 221 transitions.
[2025-04-28 21:21:52,282 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:52,282 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 15 states have internal predecessors, (19), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (13), 6 states have call predecessors, (13), 10 states have call successors, (13) Word has length 28
[2025-04-28 21:21:52,282 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:52,283 INFO  L225             Difference]: With dead ends: 112
[2025-04-28 21:21:52,284 INFO  L226             Difference]: Without dead ends: 110
[2025-04-28 21:21:52,284 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 69 GetRequests, 48 SyntacticMatches, 4 SemanticMatches, 17 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 40 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=71, Invalid=271, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:52,284 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 6 mSDsluCounter, 295 mSDsCounter, 0 mSdLazyCounter, 214 mSolverCounterSat, 24 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 337 SdHoareTripleChecker+Invalid, 238 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 24 IncrementalHoareTripleChecker+Valid, 214 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:52,285 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 337 Invalid, 238 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [24 Valid, 214 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:52,285 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 110 states.
[2025-04-28 21:21:52,305 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 110 to 90.
[2025-04-28 21:21:52,305 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 39 states have (on average 1.3076923076923077) internal successors, (51), 50 states have internal predecessors, (51), 17 states have call successors, (17), 6 states have call predecessors, (17), 33 states have return successors, (110), 33 states have call predecessors, (110), 17 states have call successors, (110)
[2025-04-28 21:21:52,306 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 178 transitions.
[2025-04-28 21:21:52,306 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 178 transitions. Word has length 28
[2025-04-28 21:21:52,307 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:52,307 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 178 transitions.
[2025-04-28 21:21:52,307 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 7 states have (on average 2.7142857142857144) internal successors, (19), 15 states have internal predecessors, (19), 10 states have call successors, (11), 1 states have call predecessors, (11), 7 states have return successors, (13), 6 states have call predecessors, (13), 10 states have call successors, (13)
[2025-04-28 21:21:52,307 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 178 transitions.
[2025-04-28 21:21:52,309 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:52,309 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:52,309 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:52,314 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:52,513 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable12
[2025-04-28 21:21:52,513 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,514 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,514 INFO  L85        PathProgramCache]: Analyzing trace with hash 1103674119, now seen corresponding path program 1 times
[2025-04-28 21:21:52,514 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,514 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [787899615]
[2025-04-28 21:21:52,514 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,514 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,518 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:52,522 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:52,523 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,523 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,603 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:52,603 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,603 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [787899615]
[2025-04-28 21:21:52,603 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [787899615] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,603 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1388452766]
[2025-04-28 21:21:52,603 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,604 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,606 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,608 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:52,612 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,663 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:52,681 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:52,681 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,681 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,683 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,684 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,754 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:52,755 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,383 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:53,383 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1388452766] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,383 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,383 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 13
[2025-04-28 21:21:53,383 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1370876826]
[2025-04-28 21:21:53,383 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,384 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:53,384 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,385 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:53,386 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=32, Invalid=124, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:53,386 INFO  L87              Difference]: Start difference. First operand 90 states and 178 transitions. Second operand  has 13 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 13 states have internal predecessors, (19), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 5 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:53,698 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:53,698 INFO  L93              Difference]: Finished difference Result 124 states and 254 transitions.
[2025-04-28 21:21:53,699 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:21:53,699 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 13 states have internal predecessors, (19), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 5 states have call predecessors, (12), 9 states have call successors, (12) Word has length 28
[2025-04-28 21:21:53,699 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:53,701 INFO  L225             Difference]: With dead ends: 124
[2025-04-28 21:21:53,701 INFO  L226             Difference]: Without dead ends: 112
[2025-04-28 21:21:53,701 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 50 SyntacticMatches, 2 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 28 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=49, Invalid=191, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:53,702 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 10 mSDsluCounter, 227 mSDsCounter, 0 mSdLazyCounter, 232 mSolverCounterSat, 31 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 34 SdHoareTripleChecker+Valid, 271 SdHoareTripleChecker+Invalid, 263 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 31 IncrementalHoareTripleChecker+Valid, 232 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:53,702 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [34 Valid, 271 Invalid, 263 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [31 Valid, 232 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:21:53,702 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-04-28 21:21:53,713 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 90.
[2025-04-28 21:21:53,713 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 39 states have (on average 1.3333333333333333) internal successors, (52), 50 states have internal predecessors, (52), 18 states have call successors, (18), 7 states have call predecessors, (18), 32 states have return successors, (107), 32 states have call predecessors, (107), 18 states have call successors, (107)
[2025-04-28 21:21:53,714 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 177 transitions.
[2025-04-28 21:21:53,715 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 177 transitions. Word has length 28
[2025-04-28 21:21:53,715 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:53,715 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 177 transitions.
[2025-04-28 21:21:53,715 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 6 states have (on average 3.1666666666666665) internal successors, (19), 13 states have internal predecessors, (19), 9 states have call successors, (11), 1 states have call predecessors, (11), 6 states have return successors, (12), 5 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:53,715 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 177 transitions.
[2025-04-28 21:21:53,716 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:53,717 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:53,717 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:53,722 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:53,920 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable13,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:53,920 INFO  L403      AbstractCegarLoop]: === Iteration 14 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:53,921 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:53,921 INFO  L85        PathProgramCache]: Analyzing trace with hash -1061542319, now seen corresponding path program 1 times
[2025-04-28 21:21:53,921 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:53,921 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [442869205]
[2025-04-28 21:21:53,921 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:53,921 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:53,925 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:53,930 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:53,930 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:53,930 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,018 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:54,018 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,018 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [442869205]
[2025-04-28 21:21:54,018 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [442869205] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:54,018 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:54,019 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:54,019 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [208633787]
[2025-04-28 21:21:54,019 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:54,019 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:54,019 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:54,019 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:54,020 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:54,020 INFO  L87              Difference]: Start difference. First operand 90 states and 177 transitions. Second operand  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:54,246 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:54,246 INFO  L93              Difference]: Finished difference Result 100 states and 186 transitions.
[2025-04-28 21:21:54,247 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:54,247 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7) Word has length 28
[2025-04-28 21:21:54,247 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:54,248 INFO  L225             Difference]: With dead ends: 100
[2025-04-28 21:21:54,248 INFO  L226             Difference]: Without dead ends: 90
[2025-04-28 21:21:54,249 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 3 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:54,249 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 7 mSDsluCounter, 167 mSDsCounter, 0 mSdLazyCounter, 194 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 19 SdHoareTripleChecker+Valid, 205 SdHoareTripleChecker+Invalid, 203 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 194 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:54,249 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [19 Valid, 205 Invalid, 203 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 194 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:54,251 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 90 states.
[2025-04-28 21:21:54,261 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 90 to 84.
[2025-04-28 21:21:54,261 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 84 states, 36 states have (on average 1.3611111111111112) internal successors, (49), 47 states have internal predecessors, (49), 18 states have call successors, (18), 7 states have call predecessors, (18), 29 states have return successors, (85), 29 states have call predecessors, (85), 18 states have call successors, (85)
[2025-04-28 21:21:54,262 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 84 states to 84 states and 152 transitions.
[2025-04-28 21:21:54,262 INFO  L79                 Accepts]: Start accepts. Automaton has 84 states and 152 transitions. Word has length 28
[2025-04-28 21:21:54,263 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:54,263 INFO  L485      AbstractCegarLoop]: Abstraction has 84 states and 152 transitions.
[2025-04-28 21:21:54,263 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:54,263 INFO  L278                IsEmpty]: Start isEmpty. Operand 84 states and 152 transitions.
[2025-04-28 21:21:54,265 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:54,265 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:54,265 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:54,265 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable14
[2025-04-28 21:21:54,265 INFO  L403      AbstractCegarLoop]: === Iteration 15 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:54,266 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:54,266 INFO  L85        PathProgramCache]: Analyzing trace with hash -676995231, now seen corresponding path program 1 times
[2025-04-28 21:21:54,266 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:54,266 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [409402440]
[2025-04-28 21:21:54,266 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,266 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:54,274 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:54,278 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:54,278 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,278 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,390 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:54,391 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:54,391 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [409402440]
[2025-04-28 21:21:54,391 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [409402440] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:54,391 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1013620652]
[2025-04-28 21:21:54,391 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:54,391 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:54,393 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:54,395 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:54,398 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:54,453 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:54,471 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:54,472 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:54,472 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:54,473 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:54,474 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:54,527 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:54,527 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:55,438 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:55,438 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1013620652] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:55,438 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:55,438 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 9] total 13
[2025-04-28 21:21:55,438 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1426078396]
[2025-04-28 21:21:55,438 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,439 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:55,439 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,439 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:55,439 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=126, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:55,440 INFO  L87              Difference]: Start difference. First operand 84 states and 152 transitions. Second operand  has 13 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 13 states have internal predecessors, (17), 7 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:55,660 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,660 INFO  L93              Difference]: Finished difference Result 122 states and 235 transitions.
[2025-04-28 21:21:55,661 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:55,661 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 13 states have internal predecessors, (17), 7 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 7 states have call successors, (12) Word has length 28
[2025-04-28 21:21:55,661 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,662 INFO  L225             Difference]: With dead ends: 122
[2025-04-28 21:21:55,662 INFO  L226             Difference]: Without dead ends: 120
[2025-04-28 21:21:55,663 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 49 SyntacticMatches, 5 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 21 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=35, Invalid=147, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:55,663 INFO  L437           NwaCegarLoop]: 39 mSDtfsCounter, 4 mSDsluCounter, 286 mSDsCounter, 0 mSdLazyCounter, 223 mSolverCounterSat, 16 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 325 SdHoareTripleChecker+Invalid, 239 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 16 IncrementalHoareTripleChecker+Valid, 223 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,663 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 325 Invalid, 239 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [16 Valid, 223 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:55,664 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 120 states.
[2025-04-28 21:21:55,677 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 120 to 90.
[2025-04-28 21:21:55,678 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 90 states, 39 states have (on average 1.3333333333333333) internal successors, (52), 50 states have internal predecessors, (52), 18 states have call successors, (18), 7 states have call predecessors, (18), 32 states have return successors, (102), 32 states have call predecessors, (102), 18 states have call successors, (102)
[2025-04-28 21:21:55,680 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 90 states to 90 states and 172 transitions.
[2025-04-28 21:21:55,682 INFO  L79                 Accepts]: Start accepts. Automaton has 90 states and 172 transitions. Word has length 28
[2025-04-28 21:21:55,682 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,682 INFO  L485      AbstractCegarLoop]: Abstraction has 90 states and 172 transitions.
[2025-04-28 21:21:55,682 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 13 states have internal predecessors, (17), 7 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:55,683 INFO  L278                IsEmpty]: Start isEmpty. Operand 90 states and 172 transitions.
[2025-04-28 21:21:55,684 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:55,684 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,684 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,689 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Ended with exit code 0
[2025-04-28 21:21:55,884 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable15
[2025-04-28 21:21:55,885 INFO  L403      AbstractCegarLoop]: === Iteration 16 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,885 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,885 INFO  L85        PathProgramCache]: Analyzing trace with hash 1607756715, now seen corresponding path program 1 times
[2025-04-28 21:21:55,885 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,885 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1958308350]
[2025-04-28 21:21:55,885 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,885 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,889 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:55,894 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:55,894 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:55,894 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,983 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:55,983 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,983 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1958308350]
[2025-04-28 21:21:55,984 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1958308350] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,984 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [548528867]
[2025-04-28 21:21:55,984 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:55,984 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,986 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,988 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:55,992 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,053 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:56,076 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:56,076 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,076 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,077 INFO  L256         TraceCheckSpWp]: Trace formula consists of 134 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,079 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,215 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:56,215 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:57,179 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:57,181 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [548528867] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:57,181 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:57,182 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 9] total 19
[2025-04-28 21:21:57,182 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1532289382]
[2025-04-28 21:21:57,182 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,182 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:21:57,182 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,183 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:21:57,183 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=41, Invalid=301, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:21:57,184 INFO  L87              Difference]: Start difference. First operand 90 states and 172 transitions. Second operand  has 19 states, 10 states have (on average 2.4) internal successors, (24), 19 states have internal predecessors, (24), 10 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (15), 7 states have call predecessors, (15), 10 states have call successors, (15)
[2025-04-28 21:21:57,775 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,775 INFO  L93              Difference]: Finished difference Result 180 states and 367 transitions.
[2025-04-28 21:21:57,776 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 24 states. 
[2025-04-28 21:21:57,776 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 10 states have (on average 2.4) internal successors, (24), 19 states have internal predecessors, (24), 10 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (15), 7 states have call predecessors, (15), 10 states have call successors, (15) Word has length 28
[2025-04-28 21:21:57,776 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,779 INFO  L225             Difference]: With dead ends: 180
[2025-04-28 21:21:57,779 INFO  L226             Difference]: Without dead ends: 170
[2025-04-28 21:21:57,780 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 78 GetRequests, 44 SyntacticMatches, 4 SemanticMatches, 30 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 101 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=124, Invalid=868, Unknown=0, NotChecked=0, Total=992
[2025-04-28 21:21:57,782 INFO  L437           NwaCegarLoop]: 38 mSDtfsCounter, 24 mSDsluCounter, 378 mSDsCounter, 0 mSdLazyCounter, 290 mSolverCounterSat, 92 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 24 SdHoareTripleChecker+Valid, 416 SdHoareTripleChecker+Invalid, 382 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 92 IncrementalHoareTripleChecker+Valid, 290 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,783 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [24 Valid, 416 Invalid, 382 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [92 Valid, 290 Invalid, 0 Unknown, 0 Unchecked, 0.4s Time]
[2025-04-28 21:21:57,784 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 170 states.
[2025-04-28 21:21:57,810 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 170 to 92.
[2025-04-28 21:21:57,811 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 92 states, 40 states have (on average 1.325) internal successors, (53), 51 states have internal predecessors, (53), 18 states have call successors, (18), 7 states have call predecessors, (18), 33 states have return successors, (103), 33 states have call predecessors, (103), 18 states have call successors, (103)
[2025-04-28 21:21:57,813 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 92 states to 92 states and 174 transitions.
[2025-04-28 21:21:57,814 INFO  L79                 Accepts]: Start accepts. Automaton has 92 states and 174 transitions. Word has length 28
[2025-04-28 21:21:57,814 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,814 INFO  L485      AbstractCegarLoop]: Abstraction has 92 states and 174 transitions.
[2025-04-28 21:21:57,815 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 10 states have (on average 2.4) internal successors, (24), 19 states have internal predecessors, (24), 10 states have call successors, (13), 1 states have call predecessors, (13), 9 states have return successors, (15), 7 states have call predecessors, (15), 10 states have call successors, (15)
[2025-04-28 21:21:57,815 INFO  L278                IsEmpty]: Start isEmpty. Operand 92 states and 174 transitions.
[2025-04-28 21:21:57,816 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:57,816 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,817 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,823 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:58,020 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable16
[2025-04-28 21:21:58,021 INFO  L403      AbstractCegarLoop]: === Iteration 17 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,021 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,021 INFO  L85        PathProgramCache]: Analyzing trace with hash -1682102906, now seen corresponding path program 1 times
[2025-04-28 21:21:58,021 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,021 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [425723100]
[2025-04-28 21:21:58,021 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,021 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,026 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:58,031 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:58,031 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,031 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,133 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:58,133 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:58,133 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [425723100]
[2025-04-28 21:21:58,134 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [425723100] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:58,134 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1230549026]
[2025-04-28 21:21:58,134 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:58,134 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,136 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:58,139 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:58,143 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:58,214 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:58,233 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:58,233 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:58,233 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:58,235 INFO  L256         TraceCheckSpWp]: Trace formula consists of 130 conjuncts, 10 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:58,236 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:58,289 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:58,289 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:59,188 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:59,188 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1230549026] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:59,188 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:59,188 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [9, 9, 9] total 13
[2025-04-28 21:21:59,190 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [869888846]
[2025-04-28 21:21:59,191 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,191 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:21:59,191 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,191 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:21:59,192 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=126, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:21:59,192 INFO  L87              Difference]: Start difference. First operand 92 states and 174 transitions. Second operand  has 13 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 13 states have internal predecessors, (17), 7 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:59,432 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,433 INFO  L93              Difference]: Finished difference Result 118 states and 226 transitions.
[2025-04-28 21:21:59,433 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:59,433 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 13 states have internal predecessors, (17), 7 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 7 states have call successors, (12) Word has length 28
[2025-04-28 21:21:59,433 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,435 INFO  L225             Difference]: With dead ends: 118
[2025-04-28 21:21:59,435 INFO  L226             Difference]: Without dead ends: 112
[2025-04-28 21:21:59,435 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 66 GetRequests, 49 SyntacticMatches, 5 SemanticMatches, 12 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 21 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=35, Invalid=147, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:59,436 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 5 mSDsluCounter, 317 mSDsCounter, 0 mSdLazyCounter, 231 mSolverCounterSat, 14 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 9 SdHoareTripleChecker+Valid, 361 SdHoareTripleChecker+Invalid, 245 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 14 IncrementalHoareTripleChecker+Valid, 231 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,436 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [9 Valid, 361 Invalid, 245 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [14 Valid, 231 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:59,437 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 112 states.
[2025-04-28 21:21:59,445 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 112 to 82.
[2025-04-28 21:21:59,445 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 35 states have (on average 1.3714285714285714) internal successors, (48), 46 states have internal predecessors, (48), 18 states have call successors, (18), 7 states have call predecessors, (18), 28 states have return successors, (87), 28 states have call predecessors, (87), 18 states have call successors, (87)
[2025-04-28 21:21:59,446 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 153 transitions.
[2025-04-28 21:21:59,447 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 153 transitions. Word has length 28
[2025-04-28 21:21:59,447 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,447 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 153 transitions.
[2025-04-28 21:21:59,447 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 7 states have (on average 2.4285714285714284) internal successors, (17), 13 states have internal predecessors, (17), 7 states have call successors, (10), 1 states have call predecessors, (10), 6 states have return successors, (12), 5 states have call predecessors, (12), 7 states have call successors, (12)
[2025-04-28 21:21:59,447 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 153 transitions.
[2025-04-28 21:21:59,448 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:59,449 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,449 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,454 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:59,652 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable17
[2025-04-28 21:21:59,652 INFO  L403      AbstractCegarLoop]: === Iteration 18 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,653 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,653 INFO  L85        PathProgramCache]: Analyzing trace with hash -2051914095, now seen corresponding path program 2 times
[2025-04-28 21:21:59,653 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,653 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [483019134]
[2025-04-28 21:21:59,653 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:59,653 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,659 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 32 statements into 2 equivalence classes.
[2025-04-28 21:21:59,664 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:21:59,665 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:59,665 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,751 INFO  L134       CoverageAnalysis]: Checked inductivity of 13 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 11 trivial. 0 not checked.
[2025-04-28 21:21:59,751 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,751 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [483019134]
[2025-04-28 21:21:59,751 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [483019134] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:59,751 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:59,752 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [8] imperfect sequences [] total 8
[2025-04-28 21:21:59,752 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [367711281]
[2025-04-28 21:21:59,752 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:59,752 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 8 states
[2025-04-28 21:21:59,753 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:59,753 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 8 interpolants.
[2025-04-28 21:21:59,754 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=13, Invalid=43, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:59,754 INFO  L87              Difference]: Start difference. First operand 82 states and 153 transitions. Second operand  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:59,973 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:59,973 INFO  L93              Difference]: Finished difference Result 102 states and 187 transitions.
[2025-04-28 21:21:59,973 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:59,974 INFO  L79                 Accepts]: Start accepts. Automaton has  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7) Word has length 32
[2025-04-28 21:21:59,974 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:59,975 INFO  L225             Difference]: With dead ends: 102
[2025-04-28 21:21:59,976 INFO  L226             Difference]: Without dead ends: 94
[2025-04-28 21:21:59,976 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=21, Invalid=69, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:59,977 INFO  L437           NwaCegarLoop]: 40 mSDtfsCounter, 7 mSDsluCounter, 177 mSDsCounter, 0 mSdLazyCounter, 177 mSolverCounterSat, 9 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 217 SdHoareTripleChecker+Invalid, 186 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 9 IncrementalHoareTripleChecker+Valid, 177 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:59,977 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 217 Invalid, 186 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [9 Valid, 177 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:21:59,978 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 94 states.
[2025-04-28 21:21:59,988 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 94 to 82.
[2025-04-28 21:21:59,988 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 82 states, 35 states have (on average 1.3714285714285714) internal successors, (48), 46 states have internal predecessors, (48), 18 states have call successors, (18), 7 states have call predecessors, (18), 28 states have return successors, (86), 28 states have call predecessors, (86), 18 states have call successors, (86)
[2025-04-28 21:21:59,991 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 82 states to 82 states and 152 transitions.
[2025-04-28 21:21:59,991 INFO  L79                 Accepts]: Start accepts. Automaton has 82 states and 152 transitions. Word has length 32
[2025-04-28 21:21:59,991 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:59,991 INFO  L485      AbstractCegarLoop]: Abstraction has 82 states and 152 transitions.
[2025-04-28 21:21:59,991 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 8 states, 5 states have (on average 2.6) internal successors, (13), 8 states have internal predecessors, (13), 4 states have call successors, (7), 1 states have call predecessors, (7), 4 states have return successors, (7), 3 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:59,992 INFO  L278                IsEmpty]: Start isEmpty. Operand 82 states and 152 transitions.
[2025-04-28 21:21:59,993 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:21:59,993 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:59,993 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:59,993 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable18
[2025-04-28 21:21:59,993 INFO  L403      AbstractCegarLoop]: === Iteration 19 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:59,994 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:59,994 INFO  L85        PathProgramCache]: Analyzing trace with hash -1661549867, now seen corresponding path program 1 times
[2025-04-28 21:21:59,994 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:59,994 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [675937599]
[2025-04-28 21:21:59,994 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:59,994 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:59,999 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:00,008 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:00,008 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,008 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,096 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:00,096 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:00,096 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [675937599]
[2025-04-28 21:22:00,096 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [675937599] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:00,096 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [222149988]
[2025-04-28 21:22:00,096 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:00,096 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:00,099 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:00,101 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:00,105 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:22:00,188 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:00,210 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:00,210 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:00,210 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:00,211 INFO  L256         TraceCheckSpWp]: Trace formula consists of 164 conjuncts, 9 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:00,216 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:00,290 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:00,292 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:00,925 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 2 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:22:00,925 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [222149988] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:00,925 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:00,925 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 8, 8] total 13
[2025-04-28 21:22:00,925 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [358894625]
[2025-04-28 21:22:00,925 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:00,926 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 13 states
[2025-04-28 21:22:00,926 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:00,926 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 13 interpolants.
[2025-04-28 21:22:00,926 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=32, Invalid=124, Unknown=0, NotChecked=0, Total=156
[2025-04-28 21:22:00,927 INFO  L87              Difference]: Start difference. First operand 82 states and 152 transitions. Second operand  has 13 states, 6 states have (on average 3.3333333333333335) internal successors, (20), 13 states have internal predecessors, (20), 9 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:22:01,178 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:01,179 INFO  L93              Difference]: Finished difference Result 96 states and 169 transitions.
[2025-04-28 21:22:01,179 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 12 states. 
[2025-04-28 21:22:01,179 INFO  L79                 Accepts]: Start accepts. Automaton has  has 13 states, 6 states have (on average 3.3333333333333335) internal successors, (20), 13 states have internal predecessors, (20), 9 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13) Word has length 32
[2025-04-28 21:22:01,179 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:01,181 INFO  L225             Difference]: With dead ends: 96
[2025-04-28 21:22:01,181 INFO  L226             Difference]: Without dead ends: 88
[2025-04-28 21:22:01,181 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 74 GetRequests, 58 SyntacticMatches, 2 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 28 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=49, Invalid=191, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:22:01,182 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 10 mSDsluCounter, 221 mSDsCounter, 0 mSdLazyCounter, 214 mSolverCounterSat, 36 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 29 SdHoareTripleChecker+Valid, 265 SdHoareTripleChecker+Invalid, 250 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 36 IncrementalHoareTripleChecker+Valid, 214 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.2s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:01,182 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [29 Valid, 265 Invalid, 250 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [36 Valid, 214 Invalid, 0 Unknown, 0 Unchecked, 0.2s Time]
[2025-04-28 21:22:01,182 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 88 states.
[2025-04-28 21:22:01,189 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 88 to 76.
[2025-04-28 21:22:01,189 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 76 states, 32 states have (on average 1.40625) internal successors, (45), 43 states have internal predecessors, (45), 18 states have call successors, (18), 7 states have call predecessors, (18), 25 states have return successors, (67), 25 states have call predecessors, (67), 18 states have call successors, (67)
[2025-04-28 21:22:01,190 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 76 states to 76 states and 130 transitions.
[2025-04-28 21:22:01,190 INFO  L79                 Accepts]: Start accepts. Automaton has 76 states and 130 transitions. Word has length 32
[2025-04-28 21:22:01,190 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:01,191 INFO  L485      AbstractCegarLoop]: Abstraction has 76 states and 130 transitions.
[2025-04-28 21:22:01,191 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 13 states, 6 states have (on average 3.3333333333333335) internal successors, (20), 13 states have internal predecessors, (20), 9 states have call successors, (12), 1 states have call predecessors, (12), 6 states have return successors, (13), 6 states have call predecessors, (13), 9 states have call successors, (13)
[2025-04-28 21:22:01,191 INFO  L278                IsEmpty]: Start isEmpty. Operand 76 states and 130 transitions.
[2025-04-28 21:22:01,192 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 33
[2025-04-28 21:22:01,192 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:01,192 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:01,198 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:01,392 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable19,10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,393 INFO  L403      AbstractCegarLoop]: === Iteration 20 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:01,393 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:01,393 INFO  L85        PathProgramCache]: Analyzing trace with hash -1801113158, now seen corresponding path program 1 times
[2025-04-28 21:22:01,393 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:01,393 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1656729189]
[2025-04-28 21:22:01,393 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,393 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:01,398 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:01,404 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:01,404 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,404 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,545 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:01,545 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:01,545 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1656729189]
[2025-04-28 21:22:01,545 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1656729189] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:01,545 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1712454813]
[2025-04-28 21:22:01,545 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:01,545 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:01,548 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:01,550 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:01,555 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:22:01,642 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 32 statements into 1 equivalence classes.
[2025-04-28 21:22:01,662 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 32 of 32 statements.
[2025-04-28 21:22:01,662 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:01,662 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:01,663 INFO  L256         TraceCheckSpWp]: Trace formula consists of 156 conjuncts, 19 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:01,667 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:01,765 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:01,765 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:04,168 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:04,168 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1712454813] provided 1 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:04,168 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 2 imperfect interpolant sequences.
[2025-04-28 21:22:04,169 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [9] imperfect sequences [9, 9] total 16
[2025-04-28 21:22:04,169 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1248205744]
[2025-04-28 21:22:04,169 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:04,169 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:22:04,169 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:04,170 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:22:04,170 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=43, Invalid=197, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:22:04,170 INFO  L87              Difference]: Start difference. First operand 76 states and 130 transitions. Second operand  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:22:04,318 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,318 INFO  L93              Difference]: Finished difference Result 82 states and 136 transitions.
[2025-04-28 21:22:04,319 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 9 states. 
[2025-04-28 21:22:04,319 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8) Word has length 32
[2025-04-28 21:22:04,319 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,320 INFO  L225             Difference]: With dead ends: 82
[2025-04-28 21:22:04,320 INFO  L226             Difference]: Without dead ends: 77
[2025-04-28 21:22:04,320 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 74 GetRequests, 55 SyntacticMatches, 5 SemanticMatches, 14 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 36 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=43, Invalid=197, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:22:04,321 INFO  L437           NwaCegarLoop]: 37 mSDtfsCounter, 2 mSDsluCounter, 170 mSDsCounter, 0 mSdLazyCounter, 126 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 207 SdHoareTripleChecker+Invalid, 131 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 126 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,321 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 207 Invalid, 131 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 126 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:04,322 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 77 states.
[2025-04-28 21:22:04,326 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 77 to 65.
[2025-04-28 21:22:04,326 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 65 states, 27 states have (on average 1.4444444444444444) internal successors, (39), 37 states have internal predecessors, (39), 17 states have call successors, (17), 7 states have call predecessors, (17), 20 states have return successors, (49), 20 states have call predecessors, (49), 17 states have call successors, (49)
[2025-04-28 21:22:04,327 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 65 states to 65 states and 105 transitions.
[2025-04-28 21:22:04,327 INFO  L79                 Accepts]: Start accepts. Automaton has 65 states and 105 transitions. Word has length 32
[2025-04-28 21:22:04,327 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,327 INFO  L485      AbstractCegarLoop]: Abstraction has 65 states and 105 transitions.
[2025-04-28 21:22:04,327 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 6 states have (on average 2.3333333333333335) internal successors, (14), 9 states have internal predecessors, (14), 4 states have call successors, (8), 1 states have call predecessors, (8), 5 states have return successors, (8), 5 states have call predecessors, (8), 4 states have call successors, (8)
[2025-04-28 21:22:04,327 INFO  L278                IsEmpty]: Start isEmpty. Operand 65 states and 105 transitions.
[2025-04-28 21:22:04,328 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:04,328 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,328 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:04,334 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-04-28 21:22:04,530 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable20,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,530 INFO  L403      AbstractCegarLoop]: === Iteration 21 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,530 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,530 INFO  L85        PathProgramCache]: Analyzing trace with hash -301727083, now seen corresponding path program 1 times
[2025-04-28 21:22:04,530 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,530 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [392457712]
[2025-04-28 21:22:04,530 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:04,530 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,536 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:04,545 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:04,545 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:04,545 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,651 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 0 refuted. 0 times theorem prover too weak. 14 trivial. 0 not checked.
[2025-04-28 21:22:04,651 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,651 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [392457712]
[2025-04-28 21:22:04,651 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [392457712] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:22:04,651 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:22:04,651 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:22:04,651 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1695245072]
[2025-04-28 21:22:04,651 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:22:04,652 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:22:04,652 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:04,652 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:22:04,652 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:22:04,652 INFO  L87              Difference]: Start difference. First operand 65 states and 105 transitions. Second operand  has 7 states, 5 states have (on average 2.8) internal successors, (14), 7 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:22:04,784 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:04,784 INFO  L93              Difference]: Finished difference Result 67 states and 106 transitions.
[2025-04-28 21:22:04,785 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:22:04,785 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 2.8) internal successors, (14), 7 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8) Word has length 36
[2025-04-28 21:22:04,785 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:04,786 INFO  L225             Difference]: With dead ends: 67
[2025-04-28 21:22:04,786 INFO  L226             Difference]: Without dead ends: 58
[2025-04-28 21:22:04,786 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 11 GetRequests, 5 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:22:04,787 INFO  L437           NwaCegarLoop]: 39 mSDtfsCounter, 2 mSDsluCounter, 143 mSDsCounter, 0 mSdLazyCounter, 111 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 5 SdHoareTripleChecker+Valid, 182 SdHoareTripleChecker+Invalid, 116 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 111 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:04,787 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [5 Valid, 182 Invalid, 116 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 111 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:04,788 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-04-28 21:22:04,793 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 56.
[2025-04-28 21:22:04,793 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 23 states have (on average 1.4782608695652173) internal successors, (34), 32 states have internal predecessors, (34), 16 states have call successors, (16), 7 states have call predecessors, (16), 16 states have return successors, (41), 17 states have call predecessors, (41), 16 states have call successors, (41)
[2025-04-28 21:22:04,794 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 91 transitions.
[2025-04-28 21:22:04,794 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 91 transitions. Word has length 36
[2025-04-28 21:22:04,794 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:04,794 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 91 transitions.
[2025-04-28 21:22:04,794 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 2.8) internal successors, (14), 7 states have internal predecessors, (14), 3 states have call successors, (8), 1 states have call predecessors, (8), 4 states have return successors, (8), 4 states have call predecessors, (8), 3 states have call successors, (8)
[2025-04-28 21:22:04,795 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 91 transitions.
[2025-04-28 21:22:04,795 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:04,795 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:04,795 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:04,796 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable21
[2025-04-28 21:22:04,796 INFO  L403      AbstractCegarLoop]: === Iteration 22 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:04,796 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:04,796 INFO  L85        PathProgramCache]: Analyzing trace with hash -13687420, now seen corresponding path program 2 times
[2025-04-28 21:22:04,796 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:04,796 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [419555952]
[2025-04-28 21:22:04,797 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:04,797 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:04,802 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 36 statements into 2 equivalence classes.
[2025-04-28 21:22:04,810 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:04,811 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:04,811 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:04,960 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:04,960 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:04,960 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [419555952]
[2025-04-28 21:22:04,960 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [419555952] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:04,960 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1041118120]
[2025-04-28 21:22:04,960 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:22:04,960 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:04,963 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:04,965 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:04,967 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:22:05,077 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 36 statements into 2 equivalence classes.
[2025-04-28 21:22:05,101 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:05,101 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:22:05,102 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:05,103 INFO  L256         TraceCheckSpWp]: Trace formula consists of 190 conjuncts, 13 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:05,104 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:05,174 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:05,174 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:06,335 INFO  L134       CoverageAnalysis]: Checked inductivity of 16 backedges. 2 proven. 7 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:06,335 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1041118120] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:06,335 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:06,336 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [12, 12, 12] total 19
[2025-04-28 21:22:06,336 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1244339815]
[2025-04-28 21:22:06,336 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:06,336 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 19 states
[2025-04-28 21:22:06,336 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:06,337 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 19 interpolants.
[2025-04-28 21:22:06,337 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=54, Invalid=288, Unknown=0, NotChecked=0, Total=342
[2025-04-28 21:22:06,337 INFO  L87              Difference]: Start difference. First operand 56 states and 91 transitions. Second operand  has 19 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 19 states have internal predecessors, (24), 12 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (17), 9 states have call predecessors, (17), 12 states have call successors, (17)
[2025-04-28 21:22:06,686 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:06,686 INFO  L93              Difference]: Finished difference Result 84 states and 148 transitions.
[2025-04-28 21:22:06,686 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 16 states. 
[2025-04-28 21:22:06,686 INFO  L79                 Accepts]: Start accepts. Automaton has  has 19 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 19 states have internal predecessors, (24), 12 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (17), 9 states have call predecessors, (17), 12 states have call successors, (17) Word has length 36
[2025-04-28 21:22:06,687 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:06,688 INFO  L225             Difference]: With dead ends: 84
[2025-04-28 21:22:06,688 INFO  L226             Difference]: Without dead ends: 80
[2025-04-28 21:22:06,688 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 89 GetRequests, 62 SyntacticMatches, 4 SemanticMatches, 23 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 93 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=103, Invalid=497, Unknown=0, NotChecked=0, Total=600
[2025-04-28 21:22:06,689 INFO  L437           NwaCegarLoop]: 44 mSDtfsCounter, 10 mSDsluCounter, 445 mSDsCounter, 0 mSdLazyCounter, 359 mSolverCounterSat, 26 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 489 SdHoareTripleChecker+Invalid, 385 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 26 IncrementalHoareTripleChecker+Valid, 359 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:06,690 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 489 Invalid, 385 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [26 Valid, 359 Invalid, 0 Unknown, 0 Unchecked, 0.3s Time]
[2025-04-28 21:22:06,691 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 80 states.
[2025-04-28 21:22:06,698 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 80 to 64.
[2025-04-28 21:22:06,698 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 64 states, 27 states have (on average 1.4074074074074074) internal successors, (38), 36 states have internal predecessors, (38), 16 states have call successors, (16), 7 states have call predecessors, (16), 20 states have return successors, (54), 21 states have call predecessors, (54), 16 states have call successors, (54)
[2025-04-28 21:22:06,699 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 64 states to 64 states and 108 transitions.
[2025-04-28 21:22:06,699 INFO  L79                 Accepts]: Start accepts. Automaton has 64 states and 108 transitions. Word has length 36
[2025-04-28 21:22:06,699 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:06,699 INFO  L485      AbstractCegarLoop]: Abstraction has 64 states and 108 transitions.
[2025-04-28 21:22:06,699 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 19 states, 9 states have (on average 2.6666666666666665) internal successors, (24), 19 states have internal predecessors, (24), 12 states have call successors, (14), 1 states have call predecessors, (14), 9 states have return successors, (17), 9 states have call predecessors, (17), 12 states have call successors, (17)
[2025-04-28 21:22:06,700 INFO  L278                IsEmpty]: Start isEmpty. Operand 64 states and 108 transitions.
[2025-04-28 21:22:06,700 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 37
[2025-04-28 21:22:06,700 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:06,700 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:06,708 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Forceful destruction successful, exit code 0
[2025-04-28 21:22:06,901 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 12 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable22
[2025-04-28 21:22:06,901 INFO  L403      AbstractCegarLoop]: === Iteration 23 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:06,901 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:06,901 INFO  L85        PathProgramCache]: Analyzing trace with hash 894023327, now seen corresponding path program 1 times
[2025-04-28 21:22:06,901 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:06,901 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1897241081]
[2025-04-28 21:22:06,901 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:06,901 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:06,906 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:06,917 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:06,917 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:06,917 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,406 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:07,406 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:07,406 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1897241081]
[2025-04-28 21:22:07,406 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1897241081] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:07,406 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1140226204]
[2025-04-28 21:22:07,406 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:22:07,406 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:07,408 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:07,410 INFO  L229       MonitoredProcess]: Starting monitored process 13 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:22:07,412 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (13)] Waiting until timeout for monitored process
[2025-04-28 21:22:07,532 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 36 statements into 1 equivalence classes.
[2025-04-28 21:22:07,555 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 36 of 36 statements.
[2025-04-28 21:22:07,556 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:22:07,556 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:07,558 INFO  L256         TraceCheckSpWp]: Trace formula consists of 186 conjuncts, 85 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:07,560 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:08,348 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 0 proven. 8 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:22:08,348 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
