Incorrect result of sum int-casted BitVec using Z3, Z3py

Question

I am using the following python code to find two binary numbers that:

sum to a certain number
their highest bits cast to integers must sum up to 2

The second constraint is more important to me; and in my case, it will scale: let's say it might become that highest bits of [N] number must sum up to [M].

I am not sure why z3 does not give the correct result. Any hints? Thanks a lot.

def BV2Int(var):
    return ArithRef(Z3_mk_bv2int(ctx.ref(), var.as_ast(), 0), var.ctx)

def main():
    s = Solver()
    s.set(':models', True) 
    s.set(':auto-cfgig', False) 
    s.set(':smt.bv.enable_int2bv',True) 

    x = BitVec('x',4)
    y = BitVec('y',4)
    s = Solver()
    s.add(x+y == 16, Extract(3,3,x) + Extract(3,3,y) == 2)
    s.check()
    print s.model()
    # result: [y = 0, x = 0], fail both constraint

    s = Solver()
    s.add(x+y == 16, BV2Int(Extract(3,3,x)) + BV2Int(Extract(3,3,y)) == 2)
    s.check()
    print s.model()
    # result: [y = 15, x = 1], fail the second constraint

Update: Thanks the answer from Christoph. Here is a quick fix:

Extract(3,3,x) -> ZeroExt(SZ, Extract(3,3,x)) where SZ is the bit width of RHS minus 1.

score 0 · Accepted Answer · edited May 23 '17 at 12:14

0

(Aside: auto-cfgig should be auto-config.)

Note that bv2int and int2bv are essentially treated as uninterpreted, so if this part is crucial to your problem, then don't use them (see documentation and previous questions).

The problem with this example are the widths of the bit-vectors. Both x and y are 4-bit variables, and the numeral 16 as a 4-bit vector is 0 (modulo 2^4), so, indeed x + y is equal to 16 when x=0 and y=0.

Further, the Extract(...) terms extract 1-bit vectors, which means that the sum Ex.. + Ex.. is again a 1-bit value and the numeral 2 as a 1-bit vector is 0 (modulo 2^1), i.e., it is indeed the case that Ex... + Ex... = 2.

edited May 23 '17 at 12:14

Community

1
1

answered Aug 07 '15 at 12:05

Christoph Wintersteiger

8,234
1
16
30

Thanks a lot! Christoph. so is the second case similar? That is we got 1 bit extracted. After wrapped up with BV2Int, we then got a 1 bit integer, so we still need to chop the RHS to become a 1 bit integer. – Zheng Cheng Aug 07 '15 at 14:19

Incorrect result of sum int-casted BitVec using Z3, Z3py

1 Answers1