From af5c6e43b91aad0a2ae16ea3a1abf6cb574d3a09 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Sep 2021 11:21:57 -0700 Subject: [PATCH] #5528 --- src/sat/sat_solver/inc_sat_solver.cpp | 2 ++ src/sat/smt/q_ematch.cpp | 12 ++++++++---- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 7999676d6..d3782cf53 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -1050,6 +1050,8 @@ private: eval.set_model_completion(true); bool all_true = true; for (expr * f : m_fmls) { + if (has_quantifiers(f)) + continue; expr_ref tmp(m); eval(f, tmp); if (m.limit().is_canceled()) diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index a2c27fd60..2e779cb80 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -359,17 +359,21 @@ namespace q { for (unsigned i = 0; i < c.num_decls(); ++i) _binding.push_back(binding[i]->get_expr()); var_subst subst(m); + auto sub = [&](expr* e) { + expr_ref r = subst(e, _binding); + //ctx.rewrite(r); + return l.sign ? ~ctx.mk_literal(r) : ctx.mk_literal(r); + }; if (m.is_true(l.rhs)) { SASSERT(!l.sign); - return ctx.mk_literal(subst(l.lhs, _binding)); + return sub(l.lhs); } else if (m.is_false(l.rhs)) { SASSERT(!l.sign); - return ~ctx.mk_literal(subst(l.lhs, _binding)); + return ~sub(l.lhs); } expr_ref fml(m.mk_eq(l.lhs, l.rhs), m); - fml = subst(fml, _binding); - return l.sign ? ~ctx.mk_literal(fml) : ctx.mk_literal(fml); + return sub(fml); } struct ematch::reset_in_queue : public trail {