False positive on QF_BVFPLRA

[aytey]

For this file:

(set-logic QF_BVFPLRA)
; (set-logic QF_LRA)
(declare-fun honk () Real)
(assert (= honk 0.75))
(check-sat)
(exit)

Dolmen reports:

File "./lra.smt2", line 4, character 16-20:
Error Real literals are not part of the Floats specification.

However, the logic LRA has been enabled (and Dolmen does not report "unknown logic"). If you comment the first line and uncomment the second (i.e., so LRA is the enabled logic), Dolmen happily accepts this file.

[Gbury]

That's a bug indeed, will look at it as soon as possible.

[Gbury]

related to #43

[Gbury]

This will be solved simply by stopping to accept real literals in the float theory. However, this problem could also be caused by bitvector literals, so I have a question: are bitvectors extended literals (i.e. (_ bv13 32)) officially allowed in the float theory ?

[aytey]

This will be solved simply by stopping to accept real literals in the float theory. However, this problem could also be caused by bitvector literals, so I have a question: are bitvectors extended literals (i.e. (_ bv13 32)) officially allowed in the float theory ?

I'm faaaaarrrrrrr from an expert, but I think not: only #bX and #xX are supported in the FP theory.