3 ms·
I'd expect a SMT (Satisfiability modulo theory) solver like z3 to work better for this use case, might be worth giving it a try. E.g. x = z3.BitVec('x', 32)
by hairtuq 9y ago
I'd expect a SMT (Satisfiability modulo theory) solver like z3 to work better for this use case, might be worth giving it a try. E.g.
x = z3.BitVec('x', 32)
y = z3.BitVec('y', 32)
i1 = x | y
i2 = ~(~x | ~y)
s = z3.Solver()
s.add(i1 != i2)
if s.check() == z3.sat:
print "found counterexample"
print s.model()
else:
print "always equal"