Skip to content

Instantly share code, notes, and snippets.

@sysopfb

sysopfb/m.py

Created November 21, 2019 15:31
Show Gist options
  • Save sysopfb/2672c6da333e6af6f7e63a900eddf511 to your computer and use it in GitHub Desktop.
Save sysopfb/2672c6da333e6af6f7e63a900eddf511 to your computer and use it in GitHub Desktop.
Download ZIP
michael
Raw
m.py
from z3 import *
x = BitVec('x',32)
y = BitVec('y',16)
s = Solver()
s.add(x * ZeroExt(16,y) == 0x7B5658DB)
s.add(ZeroExt(16,x) * ZeroExt(32, y) > 0x7B5658DB)
vals=[]
while s.check() == sat:
#print(s.model())
vals.append((s.model()[x], s.model()[y]))
s.add(Or(x != s.model()[x], y != s.model()[y]))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment