fix #3975

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 15, 2020 · 25252af · 25252af
1 parent cce27ff
commit 25252af
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
@@ -1333,7 +1333,7 @@ namespace qe {
         conjunctions                m_conjs;
 
         // maintain queue for variables.
-
+        
         app_ref_vector               m_free_vars;    // non-quantified variables
         app_ref_vector               m_trail;
 
@@ -1588,6 +1588,7 @@ namespace qe {
 
         void add_constraint(bool use_current_val, expr* l1 = nullptr, expr* l2 = nullptr, expr* l3 = nullptr) override {
             search_tree* node = m_current;           
+            expr_ref _l1(l1, m), _l2(l2, m), _l3(l3, m);
             if (!use_current_val) {
                 node = m_current->parent();
             }
@@ -1600,7 +1601,7 @@ namespace qe {
             add_literal(l2);
             add_literal(l3);
             expr_ref fml(m);
-            fml = m.mk_or(m_literals.size(), m_literals.c_ptr());
+            fml = m.mk_or(m_literals);
             TRACE("qe", tout << fml << "\n";);
             m_solver.assert_expr(fml);
         }            

diff --git a/src/qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp
@@ -650,13 +650,13 @@ namespace qe {
             SASSERT(idx <= eqs.num_eqs());
 
             if (idx < eqs.num_eqs()) {
-                expr* t = eqs.eq(idx);
-                m_ctx.add_constraint(true, m.mk_eq(x, t));
+                expr_ref eq(m.mk_eq(x, eqs.eq(idx)), m);
+                m_ctx.add_constraint(true, eq);
             }
             else {
                 for (unsigned i = 0; i < eqs.num_eqs(); ++i) {
-                    expr* t = eqs.eq(i);
-                    m_ctx.add_constraint(true, m.mk_not(m.mk_eq(x, t)));
+                    expr_ref ne(m.mk_not(m.mk_eq(x, eqs.eq(i))), m);
+                    m_ctx.add_constraint(true, ne);
                 }
             }
         }