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

deal with memory leak on exceptions
---
 src/sat/smt/q_ematch.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 83366dded..5ddc3150b 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -486,7 +486,7 @@ namespace q {
      * basic clausifier, assumes q has been normalized.
      */
     clause* ematch::clausify(quantifier* _q) {
-        clause* cl = alloc(clause, m, m_clauses.size());
+        scoped_ptr<clause> cl = alloc(clause, m, m_clauses.size());
         cl->m_literal = ctx.mk_literal(_q);
         quantifier_ref q(_q, m);
         q = m_qs.flatten(q);
@@ -514,7 +514,7 @@ namespace q {
         unsigned generation = nq ? nq->generation() : ctx.generation();
         cl->m_stat = m_qstat_gen(_q, generation);
         SASSERT(ctx.s().value(cl->m_literal) == l_true);
-        return cl;
+        return cl.detach();
     }
 
     lit ematch::clausify_literal(expr* arg) {