mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-21 07:56:34 -08:00
parent 4c29cddc08
commit 2427cd5d33
1 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/smt/arith_axioms.cpp
View file

@ -322,11 +322,7 @@ namespace arith {
return true;
}
/*
* 0 <= x&y < 2^sz
* x&y <= x
* x&y <= y
*/
void solver::mk_bv_axiom(app* n) {
unsigned sz;
expr* _x, * _y;
@ -336,6 +332,12 @@ namespace arith {
expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
if (a.is_band(n)) {
// 0 <= x&y < 2^sz
// x&y <= x
// x&y <= y
// TODO? x = y => x&y = x
add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
add_clause(mk_literal(a.mk_le(n, x)));