mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
debugging real/int interaction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2b0e1f7c2b
commit
56b977b418
|
@ -60,6 +60,11 @@ namespace pdr {
|
|||
return a.mk_add(e1, e2);
|
||||
}
|
||||
|
||||
app* mk_mul(expr* e1, expr* e2) {
|
||||
mk_coerce(e1, e2);
|
||||
return a.mk_mul(e1, e2);
|
||||
}
|
||||
|
||||
app* mk_le(expr* e1, expr* e2) {
|
||||
mk_coerce(e1, e2);
|
||||
return a.mk_le(e1, e2);
|
||||
|
@ -86,7 +91,7 @@ namespace pdr {
|
|||
tmp = e;
|
||||
}
|
||||
else {
|
||||
tmp = a.mk_mul(a.mk_numeral(c, a.is_int(e)), e);
|
||||
tmp = mk_mul(a.mk_numeral(c, c.is_int() && a.is_int(e)), e);
|
||||
}
|
||||
res = mk_add(res, tmp);
|
||||
}
|
||||
|
|
|
@ -479,8 +479,8 @@ namespace smt {
|
|||
return;
|
||||
}
|
||||
expr* to_r = m_util.mk_to_real(n);
|
||||
expr* lo = m_util.mk_le(to_r, x);
|
||||
expr* hi = m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false)));
|
||||
expr_ref lo(m_util.mk_le(to_r, x), m);
|
||||
expr_ref hi(m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false))), m);
|
||||
mk_axiom(m.mk_false(), lo);
|
||||
mk_axiom(m.mk_false(), hi);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue