This is a simple bit vector problem:
import z3
s = z3.Tactic('bv').solver()
m = z3.Function('m', z3.BitVecSort(32), z3.BitVecSort(32))
a, b = z3.BitVecs('a b', 32)
axioms = [
a == m(12432),
z3.Not(a == b)
]
s.add(axioms)
print(s.check())
Python crashes with error code 139. Please note that, this is not my real problem, so I must use bit vector tactic in my project, though it doesn't have any problem with smt tactic or even qfbv tactic.
