A potential bug in z3.parse_smt2_file

[JulyChen728]

Hi all,
we have found a potential bug in z3.parse_smt2_file.

For the smt2 file griggio/fmcad12/f23.smt2 in SMT-LIB-benchmarks/QF_FP, z3.parse_smt2_file returns a combination of caluses where the third one is x * x + y * y * y * y + x * x + fpFP(0, 127, 0) <= x * y * fpFP(0, 129, 0), different from the actual constraint in the smt2 file, which is (x * x + y * y) * (y * y + x * (x + fpFP(0, 127, 0))) <= x * y * fpFP(0, 129, 0).

Thank you very much for your time and effort! We look forward to hearing from you.

[wintersteiger]

I'm not sure whether we should print floating point operations in this "pretty" form at all. For instance, each of the * and + also depend on a rounding mode, which is not present in the output at all. Further, floating point addition is not associative, requiring lots of parentheses.

[NikolajBjorner]

This is a valid point. I take it as the Python pretty print is for visual inspection where details can be elided.
There is e.sexpr() that prints the expression in SMTLIB format where the relevant details are there.