From d02235fe08c85dbeb980a3147e279d25a74c3007 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Jan 2022 16:16:39 +0100 Subject: [PATCH] #5778 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. --- src/tactic/arith/purify_arith_tactic.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 9c07bcadc..843d32828 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -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());