mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix encoding for sdiv exposed by zQkAOXjEDwgm

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-03-19 16:00:09 -07:00
parent ffe7b46e74
commit 6eeb022048
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -473,8 +473,8 @@ namespace polysat {
rational N = rational::power_of_two(bv.get_bv_size(x));
expr_ref signx = mk_ule(bv.mk_numeral(N / 2, sz), x);
expr_ref signy = mk_ule(bv.mk_numeral(N / 2, sz), y);
expr_ref absx = mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), x), x);
expr_ref absy = mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), y), y);
expr_ref absx = mk_ite(signx, bv.mk_bv_neg(x), x);
expr_ref absy = mk_ite(signy, bv.mk_bv_neg(y), y);
expr* d = bv.mk_bv_udiv(absx, absy);
sat::literal lsignx = mk_literal(signx);
sat::literal lsigny = mk_literal(signy);