Unsoundness bug (cu_735)

[hra687261]

c_735_l_bis.smt2.txt c_735_l_bis.ae.txt

Responses:

	.smt2	.ae
AE(T)	Valid	Valid
AE(T-C)	Valid	Valid
AE(C-T)	Valid	Valid
AE(C)	Valid	Valid
CVC5	sat

T: Tableaux C: CDCL AE: Alt-Ergo (used-solver)

Comments:

• Replacing the line 13 in the ".smt2" file (line 11 in the ".ae" file) with 1 which is equal to ui_3 divided by itself if ui_3 is not zero, makes AE respond with "I don't know" with the four solvers. Removing any or both of the axioms (1st and 2nd assertions) does that too.