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;