From 41b1f47d77353e261d411fd382357626bf1c6c88 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Oct 2023 12:15:28 -0700
Subject: [PATCH] #6523

deal with memory leak when there is an exception
---
 src/sat/smt/q_ematch.cpp | 5 ++---
 src/smt/theory_lra.cpp   | 1 +
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index ec10426a7..83366dded 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -576,14 +576,13 @@ namespace q {
 
     void ematch::add(quantifier* _q) {
         TRACE("q", tout << "add " << mk_pp(_q, m) << "\n");
-        clause* c = clausify(_q);
+        scoped_ptr<clause> c = clausify(_q);
         quantifier* q = c->q();
         if (m_q2clauses.contains(q)) {
-            dealloc(c);
             return;
         }
         ensure_ground_enodes(*c);
-        m_clauses.push_back(c);
+        m_clauses.push_back(c.detach());
         m_q2clauses.insert(q, c->index());
         ctx.push(pop_clause(*this));
         init_watch(*c);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index cd4ca38c7..284c34b54 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1648,6 +1648,7 @@ public:
                 break;
             }
             
+
             switch (check_nla()) {
             case FC_DONE:
                 break;