Fatal failure at CVC4/src/theory/fp/fp_converter.cpp:160

[muchang]

Hi,
For this formula

(declare-fun a () (_ FloatingPoint 2 6))
(assert (= (fp.div RTZ a a) a))
(check-sat)

cvc4 --fp-exp throws a fatal failure:

Fatal failure within static void CVC4::theory::fp::symfpuSymbolic::traits::precondition(bool) at CVC4/src/theory/fp/fp_converter.cpp:160
Check failure
 b
Aborted

cvc4-1.7 does not have this fatal failure.

OS: Ubuntu 18.04
Revision: c3bc4ac

[martin-cs]

Yes, this is kind of a known limitation, hence why there is the --fp-exp flag. I want to get this fixed but having all of the weird and wacky floating-point formats working is a lot of work for not many users. Do you have a specific application for this or is this something generated by fuzzing / similar?

[muchang]

Hi Martin,

Thank you for your fixes and comments! The bugs were found by our fuzzer. We are developing new techniques for testing SMT solvers to help the advanced solvers, like CVC4, become better.

For such limitations of --fp-exp, it could be better at least giving a user-friendly message rather than throwing out a fatal failure.

[aniemetz]

Duplicate of #3623.