Parse error with `let` about dolmen HOT 4 CLOSED

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.

from dolmen.

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.

from dolmen.

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.

from dolmen.

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

from dolmen.