Unsoundness bug (cu_651)

[hra687261]

c_651_l_bis.smt2.txt
c_651_l_bis.ae.txt

Alt-Ergo responds with "Valid" on the ".ae" file with the four solvers. And "I don't know" on the ".smt2" file when the CDCL solver is used, and "Valid" with the other solvers.

The expected answer is "I don't know" in every case, since the goal in the ".ae" file isn't valid (it's negation is satisfiable) and
the assertion in the ".smt2" file (which is equivalent to the negation of the goal) is also satisfiable.

[Stevendeo]

I believe the smt2 file is Valid (unsat), because when ieqv0 = 0, a division by zero occurs. I am not sure Alt-Ergo manages to deduce its answer for the good reason though.

[bclement-ocp]

This no longer reproduces after e357e6a so it looks like #487 fixed it.