From 25252af1fcd30e925480e731cbb4afc0a442e0b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Apr 2020 08:06:43 -0700 Subject: [PATCH] fix #3975 Signed-off-by: Nikolaj Bjorner --- src/qe/qe.cpp | 5 +++-- src/qe/qe_datatype_plugin.cpp | 8 ++++---- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index b6046f1d9..5866dfedb 100644 --- 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 index 25332d164..c458de334 100644 --- 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); } } }