mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

#5778

Browse source 
not really specific to euf.true, but about rem(x,0) semantics that should align with mod semantics. It also reproduces without sat.euf=true.
This commit is contained in:
Nikolaj Bjorner 2022-01-22 16:16:39 +01:00
parent 85f6456655
commit d02235fe08
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -854,7 +854,10 @@ struct purify_arith_proc {
for (auto const& p : mods) {
body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body);
}
fmc->add(u().mk_mod0(), body);
body = m().mk_ite(u().mk_ge(v1, u().mk_int(0)), body, u().mk_uminus(body));
fmc->add(u().mk_rem0(), body);
}
if (!idivs.empty()) {
expr_ref body(u().mk_int(0), m());