mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

add and fix axioms

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-14 20:12:09 -08:00
parent ce1acd8c41
commit 3c21e3ae42
5 changed files with 115 additions and 87 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/intblast_solver.cpp
View file

@ -708,11 +708,11 @@ namespace intblast {
rational N = bv_size(e);
expr* x = umod(e, 0), *y = umod(e, 1);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
r = m.mk_ite(signx, a.mk_int(N - 1), a.mk_int(0));
r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0));
for (unsigned i = 0; i < sz; ++i) {
expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
r = m.mk_ite(m.mk_eq(y, a.mk_int(i)),
m.mk_ite(signx, a.mk_add(d, a.mk_int(N - rational::power_of_two(sz-i))), d),
m.mk_ite(signx, a.mk_add(d, a.mk_int(- rational::power_of_two(sz-i))), d),
r);
}
break;