From b8b6d96fba573017c6dfa2bcc0293ec677afe029 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Nov 2025 10:34:01 -0800
Subject: [PATCH] insert theory only once

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

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 6ec9b154a..c0a65cfb7 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4148,7 +4148,8 @@ namespace smt {
                 }
                 else if (ok == FC_GIVEUP) {
                     f  = THEORY;
-                    m_incomplete_theories.push_back(th);
+                    if (!m_incomplete_theories.contains(th))
+                        m_incomplete_theories.push_back(th);
                 }
             }
             else {