From 6163085ff82df93dd0eb9b81be11b315c5dbd8d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 May 2015 10:02:44 -0700 Subject: [PATCH] add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core Signed-off-by: Nikolaj Bjorner --- src/tactic/nlsat_smt/nl_purify_tactic.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index dd0a76f15..312e26ad0 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -182,6 +182,7 @@ public: } br_status reduce_app_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { + TRACE("nlsat_smt", { expr_ref tmp(m); tmp = m.mk_app(f, num, args); tout << "reduce: " << tmp << "\n";}); if (f->get_family_id() == m.get_basic_family_id()) { if (f->get_decl_kind() == OP_EQ && u().is_real(args[0])) { mk_interface_bool(f, num, args, result); @@ -557,6 +558,7 @@ private: } void rewrite_goal(rw& r, goal_ref const& g) { + r.reset(); expr_ref new_curr(m); proof_ref new_pr(m); unsigned sz = g->size();