Parse error with let

[aytey]

For the following file:

( set-logic QF_LIA)
( declare-fun a () Int )
( declare-fun b () Bool )
(assert (let ( (c (ite b 1.0 2.0))) (= 0 (* 2 c))))
( check-sat )

Dolmen gives:

File "./test.smt2", line 4, character 25-28:
Error Unbound identifier: `1.0`

[Gbury]

The problem uses the QF_LIA logic, so only the integer coefficients are recognized by the arithmetic theory. Hence 1.0, a rational/real coefficient, which is not recognized by the integer arithmetic, is treated as any unbound name (exactly the same as if you had written some_not_declared_symbol instead).
I'll try and see if it's reasonable to emit a warning in such cases.

[aytey]

Yeah, you're right; I managed to confuse myself while writing another example.

If you want to close this as "noise", that seems totally reasonable to me -- the "error" is indeed correct.

[Gbury]

The warning seems like a good idea so i'll elt this issue open until I implement it.

[Gbury]

Ok, so PR #81 adds a hint in such cases, and the error message is now:

File "tests/regression/issue77/test.smt2", line 4, character 25-28:
Error Unbound identifier: `1.0`
      Hint: The current logic does not include real arithmtic

This should hopefully help users understand what is wrong in those cases.