From 09ffec52e8f7b10e0469d9599c4640bc5e550d11 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 15 Jul 2026 20:54:23 -0700
Subject: [PATCH] disable instantiation for inconsistent states

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/qi_queue.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index cb803d755..d9520f721 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -197,6 +197,9 @@ namespace smt {
     }
 
     void qi_queue::instantiate(entry & ent) {
+        if (m_context.inconsistent()) 
+            return;
+        
         // set temporary flag to enable quantifier-specific tracing in within smt_internalizer.
         flet<bool> _coming_from_quant(m_context.m_coming_from_quant, true);