mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #2976

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-11 22:20:20 -08:00
parent 17984af4cc
commit 4f6e3cfe71
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -328,12 +328,12 @@ struct purify_arith_proc {
expr * k2 = mk_fresh_int_var(); expr * k2 = mk_fresh_int_var();
app_ref mod_app(m()); app_ref mod_app(m());
proof_ref mod_pr(m()); proof_ref mod_pr(m());
mod_app = u().mk_mod(args[0], args[1]); expr * x = args[0];
expr * y = args[1];
mod_app = u().mk_mod(x, y);
mk_def_proof(k2, mod_app, mod_pr); mk_def_proof(k2, mod_app, mod_pr);
cache_result(mod_app, k2, mod_pr); cache_result(mod_app, k2, mod_pr);
expr * x = args[0];
expr * y = args[1];
m_mods.push_back(bin_def(x, y, k2)); m_mods.push_back(bin_def(x, y, k2));
// (div x y) --> k1 | y = 0 \/ x = k1 * y + k2, // (div x y) --> k1 | y = 0 \/ x = k1 * y + k2,
// y = 0 \/ 0 <= k2, // y = 0 \/ 0 <= k2,
@ -840,7 +840,7 @@ struct purify_arith_proc {
expr_ref body(u().mk_int(0), m()); expr_ref body(u().mk_int(0), m());
expr_ref v0(m().mk_var(0, u().mk_int()), m()); expr_ref v0(m().mk_var(0, u().mk_int()), m());
expr_ref v1(m().mk_var(1, u().mk_int()), m()); expr_ref v1(m().mk_var(1, u().mk_int()), m());
for (auto const& p : divs) { 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); 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); fmc->add(u().mk_mod0(), body);