From cafe3acff1d4aedf2b08a4700574fcb41b4e4355 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Oct 2023 12:41:34 -0700
Subject: [PATCH] delay detach

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

diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 5ddc3150b..aa79bab5b 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -578,11 +578,10 @@ namespace q {
         TRACE("q", tout << "add " << mk_pp(_q, m) << "\n");
         scoped_ptr<clause> c = clausify(_q);
         quantifier* q = c->q();
-        if (m_q2clauses.contains(q)) {
+        if (m_q2clauses.contains(q)) 
             return;
-        }
         ensure_ground_enodes(*c);
-        m_clauses.push_back(c.detach());
+        m_clauses.push_back(c.get());
         m_q2clauses.insert(q, c->index());
         ctx.push(pop_clause(*this));
         init_watch(*c);
@@ -613,6 +612,7 @@ namespace q {
             if (!unary)
                 j++;
         }
+        c.detach();
     }