From eedade141c7a7564619d99fa6a5dc9d7385f7a61 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 16 Feb 2026 01:50:51 +0000
Subject: [PATCH] Restore defensive SASSERT in smt_conflict_resolution

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/smt_conflict_resolution.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index ce6248161..c8e378936 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -1333,6 +1333,7 @@ namespace smt {
         }
         else {
             pr = get_proof(consequent, conflict);
+            SASSERT(m_lit2proof[not_l] && pr);
             pr = m.mk_unit_resolution({ m_lit2proof[not_l], pr });
         }
         expr_ref_buffer lits(m);