From 24f495f95cf9ad82d3d4d25b856f2ffe7aa51fa1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Date: Fri, 24 Jul 2026 20:01:38 -0700
Subject: [PATCH] fix #10220: clear stale nla lemmas in core::propagate()
 (#10224)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

## Problem

egressions/smt2/10220.smt2 (datatype + nonlinear integer arithmetic over
`SBVRational`, expected `unsat`) crashes with an ACCESS_VIOLATION (issue
#10220). The crash only occurs with the default `theory_lra`
(`arith.solver=6`) and is independent of `arith.nl`.

## Root cause

Debug build gives a clean stack: a `SASSERT(n)` violation / null
dereference in `smt::relevancy_propagator_imp::is_relevant_core` reached
from `theory_lra::set_conflict_or_lemma ->
ctx().mark_as_relevant(literal)`. The literal's boolean variable has
`bool_var2expr(v) == nullptr`.

Tracing showed the same nla lemma core being processed twice — first at
scope 6, then, after a backtrack, again at scope 3 — where the bound
atoms internalized to build the lemma had their boolean variables
deleted by the pop:

\\\
SCOL scope=6 core=[32 27 35 30 6 14 ]
SCOL scope=3 core=[32*NULL* 27 35*NULL* 30 6 14 ]
\\\

Commit d60d6a066 (*add incremental propagate for nla to retain some
propagation lemmas*) removed the `clear()` call from `core::propagate()`
(the final-check path) while adding a symmetric
`incremental_propagate()` that keeps it. Consequently `m_lemmas`
generated at a deep scope survived a backtrack and were replayed at a
shallower scope, referencing deleted bool vars.

## Fix

Restore `clear()` at the start of `core::propagate()`. Both
`propagate()` and `incremental_propagate()` consume their lemmas
immediately via `add_lemmas()`, so lemmas never need to survive across
calls; starting each final-check propagation from a fresh lemma set
removes the stale replay.

## Validation

- `regressions/smt2/10220.smt2` -> `unsat` (was ACCESS_VIOLATION)
- `FStar.Math.Euclid-1` still `unsat`
- `FStar.Math.Euclid-2/-3` unchanged (already `unknown` on master,
verified against the pre-fix binary)

Fixes #10220.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
---
 src/math/lp/nla_core.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index f4baca1ced..46f2a7a1cf 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1525,6 +1525,7 @@ void core::set_use_nra_model(bool m) {
 
     
 bool core::propagate() {
+    clear();
     bool propagated = m_monomial_bounds.tighten_lp_bounds();
     if (m_monomial_bounds.propagate_changed_bounds())
         propagated = true;