From f044071f5ef6936cdb016cc41152ca472e06ffd2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 May 2020 18:13:12 -0700 Subject: [PATCH] fix #4260 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/recfun_rewriter.cpp | 2 +- src/smt/smt_conflict_resolution.cpp | 27 +++++++++++++++++++-------- 2 files changed, 20 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/recfun_rewriter.cpp b/src/ast/rewriter/recfun_rewriter.cpp index f22830e80..2519d0755 100644 --- a/src/ast/rewriter/recfun_rewriter.cpp +++ b/src/ast/rewriter/recfun_rewriter.cpp @@ -21,7 +21,7 @@ Author: #include "ast/rewriter/var_subst.h" br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - if (m_rec.is_defined(f)) { + if (m_rec.is_defined(f) && num_args > 0) { for (unsigned i = 0; i < num_args; ++i) { if (!m.is_value(args[i])) return BR_FAILED; diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 81481882e..8da396009 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -783,18 +783,25 @@ namespace smt { if (!pr) return nullptr; SASSERT(m.has_fact(pr)); + expr* f1 = nullptr, *f2 = nullptr; app * fact = to_app(m.get_fact(pr)); app * n1_owner = n1->get_owner(); app * n2_owner = n2->get_owner(); - bool is_eq = m.is_eq(fact); - if (!is_eq || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) { + bool is_eq = m.is_eq(fact, f1, f2); + if (is_eq && is_quantifier(f1)) { + f1 = m_ctx.get_enode(f1)->get_owner(); + } + if (is_eq && is_quantifier(f2)) { + f2 = m_ctx.get_enode(f2)->get_owner(); + } + if (!is_eq || (f1 != n2_owner && f2 != n2_owner)) { CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2), tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n"; if (fact->get_num_args() == 2) { - tout << "fact(0): #" << fact->get_arg(0)->get_id() << ", fact(1): #" << fact->get_arg(1)->get_id() << "\n"; + tout << "fact(0): #" << f1->get_id() << ", fact(1): #" << f2->get_id() << "\n"; } - tout << mk_bounded_pp(n1->get_owner(), m, 10) << "\n"; - tout << mk_bounded_pp(n2->get_owner(), m, 10) << "\n"; + tout << mk_bounded_pp(n1_owner, m, 10) << "\n"; + tout << mk_bounded_pp(n2_owner, m, 10) << "\n"; tout << mk_bounded_pp(fact, m, 10) << "\n"; tout << mk_ll_pp(pr, m, true, false);); SASSERT(m_ctx.is_true(n2) || m_ctx.is_false(n2)); @@ -807,12 +814,16 @@ namespace smt { return pr; } TRACE("norm_eq_proof", + tout << mk_bounded_pp(pr, m, 4) << "\n"; + tout << mk_bounded_pp(n1_owner, m) << "\n"; + tout << mk_bounded_pp(n2_owner, m) << "\n"; + tout << mk_bounded_pp(f1, m) << "\n"; + tout << mk_bounded_pp(f2, m) << "\n"; tout << "#" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n"; tout << mk_ll_pp(pr, m, true, false);); SASSERT(m.is_eq(fact)); - SASSERT((fact->get_arg(0) == n1->get_owner() && fact->get_arg(1) == n2->get_owner()) || - (fact->get_arg(1) == n1->get_owner() && fact->get_arg(0) == n2->get_owner())); - if (fact->get_arg(0) == n1_owner && fact->get_arg(1) == n2_owner) + SASSERT((f1 == n1_owner && f2 == n2_owner) || (f2 == n1_owner && f1 == n2_owner)); + if (f1 == n1_owner && f2 == n2_owner) return pr; pr = m.mk_symmetry(pr); m_new_proofs.push_back(pr);