Assertion failure in "src/lib/reasoners/intervalCalculus.ml", line 1175, when using the CDCL solver

[hra687261]

c_262_0_ae_bis.ae.txt

Running Alt-Ergo (built from the "next" branch) on the attached file with the command:

./alt-ergo --sat-solver CDCL c_262_0_ae_bis.ae

Causes the following error:

Fatal error: exception File "src/lib/reasoners/intervalCalculus.ml", line 1175, characters 4-10: Assertion failed

And when the other solvers are used (by replacing CDCL with Tableaux or Tableaux-CDCL or CDCL-Tableaux) then Alt-Ergo responds with "Valid".

Some additional interesting points:

• if we remove the axioms ax_1 and ax_2, then the answer in the four cases is:"I don't know".
• if we replace (ruqv0 * ruqv0) * (if true then ruqv0 else ur_3) in the line 14 with (ruqv0 * ruqv0) * ruqv0 or (ruqv0 * ruqv0), then AE takes too long to answer (more than 3 minutes) when the CDCL solver is used. And answers with "Valid" in the other cases.
• if we replace it with ruqv0 then the answer is "Valid" in every case.
• if we replace it with ur_3 then AE says:"I Don't Know" when the CDCL solver is used, and "Valid" in the other cases.