mirror of
https://github.com/Z3Prover/z3
synced 2025-04-20 23:56:37 +00:00
parent
eb3fc4f47e
commit
c8c088e80d
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
@ -1217,10 +1217,6 @@ namespace qe {
|
|||
add_lits(lits);
|
||||
svector<pair_t> 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))) {
|
||||
|
|
Loading…
Reference in a new issue