Inconsistency between SMT2 exporter and importer when using FP constant zero

[sebastianpoeplau]

I'm seeing surprising behavior that I think may be a bug when exporting to SMT2 and reimporting the result. I've been able to strip my file down to the following minimal example:

import z3

z = z3.fpPlusZero(z3.FPSort(11, 53))
s = z3.Solver()
s.add(z == z)

assert s.check() == z3.sat  # no problem

smt_export = s.to_smt2()
print(smt_export)

# parsing back raises an exception
z3.parse_smt2_string(smt_export)

I get the following output with Z3 versions 4.5.1, 4.8.4, and the latest master, all running on 64-bit Linux:

; benchmark generated from python API
(set-info :status unknown)
(assert
 (= ((_ to_fp 11 53) RTZ +zero) ((_ to_fp 11 53) RTZ +zero)))
(check-sat)

Traceback (most recent call last):
  File "z3_bug.py", line 13, in <module>
    z3.parse_smt2_string(smt_export)
  File "/usr/lib/python3.7/site-packages/z3/z3.py", line 8499, in parse_smt2_string
    return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
  File "/usr/lib/python3.7/site-packages/z3/z3core.py", line 3032, in Z3_parse_smtlib2_string
    _elems.Check(a0)
  File "/usr/lib/python3.7/site-packages/z3/z3core.py", line 1346, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'(error "line 4 column 25: sort of floating point constant was not specified")\n'

It seems wrong to me that the generated output cannot be parsed back. The example uses the Python API, but I believe the problem is independent of the bindings. In particular, the value ((_ to_fp 11 53) RTZ +zero), resulting from exporting the floating-point constant "plus zero", doesn't seem to be understood correctly by the parser. When I replace +zero with 0 in the SMT2 string, it parses just fine.

I'm not familiar enough with Z3's code to know how to investigate further. If you could give me any pointers, though, I'd be happy to try.

[wintersteiger]

Thanks for the report, this is now fixed.

@NikolajBjorner: I had always assumed that ast_smt_pp is SMT1 only, but it seems to be used for SMT2 as well. May be time to rename it?

[NikolajBjorner]

ast_smt2_pp is taken, so something else. fast_smt2_pp?

[sebastianpoeplau]

Great, thanks for the quick reaction and the fix!