Encountered issues with automatic theorem proving using dReal

[cao-jian]

I want to linearize c=ab using automatic theorem proving. Everything works fine when solving with SMT, but the same way of writing doesn't work for dReal.

`from dreal import *
a = Variable('a',Variable.Int)
b = Variable('b',Variable.Int)
c = Variable('c',Variable.Int)
X = [[Variable("x_%s_%s" %(i+1,j+1), Variable.Int) for j in range(4)] for i in range(4)]
f_sat =forall([a,b,c],
And(
Implies(And(a>=0,a<=1,b>=0,b<=1,c>=0,c<=1,c==a*b),And(
X[0][0]*a+X[0][1]*b+X[0][2]*c+X[0][3]<=0,
X[1][0]*a+X[1][1]*b+X[1][2]*c+X[1][3]<=0,
X[2][0]*a+X[2][1]*b+X[2][2]*c+X[2][3]<=0,
X[3][0]*a+X[3][1]*b+X[3][2]*c+X[3][3]<=0,
)),
Implies(And(a>=0,a<=1,b>=0,b<=1,c>=0,c<=1,
X[0][0]*a+X[0][1]*b+X[0][2]*c+X[0][3]<=0,
X[1][0]*a+X[1][1]*b+X[1][2]*c+X[1][3]<=0,
X[2][0]*a+X[2][1]*b+X[2][2]*c+X[2][3]<=0,
X[3][0]*a+X[3][1]*b+X[3][2]c+X[3][3]<=0,
),c==ab)
))

result = CheckSatisfiability(f_sat, 0.001)
print(result)`