From 9b8bfe6a2607ca876c2e1738b046fc6d716358a7 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Sun, 12 Jul 2026 01:29:30 -0700
Subject: [PATCH] smt: restore direct quantifier internalization in
 theory::mk_literal
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Commit 382abb786 routed theory::mk_literal through the new
context::non_ground_internalize helper. For a top-level quantifier
literal (e.g. the universally-quantified emptiness condition produced
by the sequence/regex solver), that helper takes the non-ground proxy
path — it allocates a fresh proxy constant, asserts proxy = quantifier
and internalizes assertions — instead of internalizing the quantifier
directly. This engages quantifier instantiation on a goal the seq
theory previously discharged instantly as incomplete, turning a fast
'unknown (incomplete (theory seq))' answer into a -T: timeout.

Restore the previous behavior for quantifier expressions by
internalizing them directly, while keeping non_ground_internalize for
all other (non-quantifier) expressions.

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

diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index cba15a0f33..3ecaf4e2bb 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -152,8 +152,12 @@ namespace smt {
         expr_ref e(_e, m);
         bool is_not = m.is_not(_e, _e);
         if (!ctx.e_internalized(_e)) {
-            auto n = ctx.non_ground_internalize(_e);
-            _e = n->get_expr();            
+            if (is_quantifier(_e))
+                ctx.internalize(_e, true);
+            else {
+                auto n = ctx.non_ground_internalize(_e);
+                _e = n->get_expr();
+            }
         }
         literal lit = ctx.get_literal(_e);
         ctx.mark_as_relevant(lit);