From c8c088e80d9bc84c1c4688277c48ed1a98c4833f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Jan 2020 17:50:00 -0800 Subject: [PATCH] fix #2891 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 3 +++ src/qe/qe_term_graph.cpp | 4 ---- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 9eb9bf70c..ada6be1bf 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1155,6 +1155,9 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res // (^ t -k) --> (^ (/ 1 t) k) result = m_util.mk_power(m_util.mk_div(m_util.mk_numeral(rational(1), false), arg1), m_util.mk_numeral(-y, false)); + result = m().mk_ite(m().mk_eq(arg1, m_util.mk_real(0)), + m_util.mk_real(1), + result); return BR_REWRITE2; } diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 9e080de5f..744219d47 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -1217,10 +1217,6 @@ namespace qe { add_lits(lits); svector todo; - // TBD: - // M(f(a1 + 5)) != M(f(x1 + 5)) => a1 + 5 != x1 + 5 part of dcert. - // collect subterms in arith, put equal function subterms in certifiability set - for (expr* e : lits) { expr* ne, *a, *b; if (m.is_not(e, ne) && m.is_eq(ne, a, b) && (is_uninterp(a) || is_uninterp(b))) {