Skip to content

Commit 5226b0c

Browse files
committed
fix for z3-solver>=4.8.10
1 parent 5db8c2e commit 5226b0c

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

tests/test_cas_smt.py

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ def test_reg_bv(x,y):
1313
assert complexity(z)<100
1414
m = solver([z==cst(0x0,32),xl==0xa,xh==0x84]).get_model()
1515
assert m is not None
16-
xv,yv = (m[v].as_long() for v in m)
16+
xv = m.eval(x.to_smtlib()).as_long()
17+
yv = m.eval(y.to_smtlib()).as_long()
1718
assert m.eval(xl.to_smtlib()).as_long() == 0xa
1819
assert m.eval(xh.to_smtlib()).as_long() == 0x84
1920
assert ((xv^0xcafebabe)+(yv+(xv>>2)))&0xffffffff == 0

0 commit comments

Comments
 (0)