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();
             }
         }