from z3 import *

a = BitVec('a', 32)
b = BitVec('b', 32)
c = BitVec('c', 32)

x1 = BitVec('x1', 32)
x2 = BitVec('x2', 32)
x3 = BitVec('x3', 32)

s = Solver()

s.add(a*x1*x1 + b*x1 + c == 0)
s.add(a*x2*x2 + b*x2 + c == 0)
s.add(a*x3*x3 + b*x3 + c == 0)

s.add(x1 != x2)
s.add(x2 != x3)
s.add(x1 != x3)

print s.check()

solution = s.model()
print solution

