diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index f166125ba..1f8f6dabe 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1756,16 +1756,16 @@ namespace smt {
 
             void insert_qinfo(qinfo * qi) {
                 // I'm assuming the number of qinfo's per quantifier is small. So, the linear search is not a big deal.
+                scoped_ptr<qinfo> q(qi);
                 ptr_vector<qinfo>::iterator it  = m_qinfo_vect.begin();            
                 ptr_vector<qinfo>::iterator end = m_qinfo_vect.end();            
                 for (; it != end; ++it) {
                     checkpoint();
                     if (qi->is_equal(*it)) {
-                        dealloc(qi);
                         return;
                     }
                 }
-                m_qinfo_vect.push_back(qi);
+                m_qinfo_vect.push_back(q.detach());
                 TRACE("model_finder", tout << "new quantifier qinfo: "; qi->display(tout); tout << "\n";);
             }
 
diff --git a/src/util/util.h b/src/util/util.h
index 0dfa8ac8c..a040a79ae 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -226,9 +226,7 @@ public:
     }
 
     ~scoped_ptr() {
-        if (m_ptr) {
-            dealloc(m_ptr);
-        }
+        dealloc(m_ptr);
     }
 
     T * operator->() const { 
@@ -253,9 +251,7 @@ public:
 
     scoped_ptr & operator=(T * n) {
         if (m_ptr != n) {
-            if (m_ptr) {
-                dealloc(m_ptr);
-            }
+            dealloc(m_ptr);
             m_ptr = n;
         }
         return *this;