Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- assert a.sort() == BitVecSort(128)
- assert b.sort() == BitVecSort(128)
- Extract( Extract(i+3,i,b)*8+7, Extract(i+3,i,b)*8, a)
- z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.
- >>> a = Int('a')
- >>> b = BitVec('b', a)
- ctypes.ArgumentError: argument 2: <class 'TypeError'>: wrong type
Add Comment
Please, Sign In to add comment
