From 639f902ad170a96ec534b7c833c0ab3507eaa37a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Dec 2012 17:01:00 -0800 Subject: [PATCH] fix bug in difference logic recognizer, assert in proof_util Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_util.cpp | 6 +++++- src/muz_qe/proof_utils.cpp | 5 +++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index fd08b1aad..1ea705e6e 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -1129,7 +1129,11 @@ namespace pdr { if (a.is_numeral(lhs) || a.is_numeral(rhs)) { return test_ineq(e); } - return test_term(lhs) && test_term(rhs); + return + test_term(lhs) && + test_term(rhs) && + !a.is_mul(lhs) && + !a.is_mul(rhs); } bool test_term(expr* e) const { diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp index 75c9cbb15..1e837b578 100644 --- a/src/muz_qe/proof_utils.cpp +++ b/src/muz_qe/proof_utils.cpp @@ -312,9 +312,10 @@ public: }; void proof_utils::reduce_hypotheses(proof_ref& pr) { - class reduce_hypotheses reduce(pr.get_manager()); + ast_manager& m = pr.get_manager(); + class reduce_hypotheses reduce(m); reduce(pr); - SASSERT(is_closed(pr.get_manager(), pr)); + CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";); } class proof_is_closed {