From c40f8a200e2ae882062cd75a00b1d48dc90689e2 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Mon, 27 Apr 2026 18:33:28 -0700
Subject: [PATCH] smt: reset give-up state when escalating final_check level
 (#9408)

theory_lra reports num_final_check_levels()==2: full nlsat (m_nra.check)
only runs at level >= 2. When a level-1 round-trip ends with FC_GIVEUP
and the loop escalates to level 2, the previously accumulated 'result',
'f', and 'm_incomplete_theories' were retained, so a subsequent
successful (FC_DONE) round at level 2 was still reported as
(incomplete (theory arithmetic)). Reset that state on each level
escalation.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/smt/smt_context.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index e9b2b851a..ec7209c93 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4175,6 +4175,14 @@ namespace smt {
                 if (level >= max_level || result == FC_DONE || can_propagate())
                     break;
                 ++level;
+                // Re-evaluate at the higher level: clear the give-up state
+                // accumulated at lower levels so a level that succeeds is
+                // not masked by a previous FC_GIVEUP. See e.g. theory_lra
+                // whose level 2 invokes the full nlsat (m_nra.check) that
+                // is skipped at level 1.
+                result = FC_DONE;
+                f      = OK;
+                m_incomplete_theories.reset();
             }
         }