Unsoundness bug (cu_685)

[hra687261]

c_685_l.smt2.txt c_685_l.ae.txt

The .ae and .smt2 files are supposed to be equivalent.

Alt-Ergo responds with "Valid" (on both the ".ae" and the ".smt2" files) when the Tableaux or the Tableaux-CDCL solver is used, it takes too long (more than 3 minutes) to answer when the CDCL-Tableaux solver is used, and answers with "I don't know" when the CDCL solver is used.

CVC5 answers with "sat" on the ".smt2" file, which is contradictory to Alt-Ergo's answer (With the Tableaux and the Tableaux-CDCL solvers).

Commentary:

• If we replace the line 13 in the ".smt2" file (and the line 12 in the ".ae" file) with iuqv0 or a constant integer, then Alt-Ergo answers with "I don't know" which is the expected response.