Unclear error message during model checking about dolmen HOT 7 OPEN

Right, I'll improve the syntax error message for that case (probably after the holidays though).

The reason for using a boolean instead of a flag is that it's easier if/when the default ever changes. That being said, I'm planning to make it so that you do not need to explicitly set the option when providing a file using the -r option, so that should help.

from dolmen.

I also found a wrong message from the type checker with this input file:

(set-logic ALL)
(declare-const x Int)
(declare-const y Bool)
(declare-fun f (Int Int) Int)
(assert (= (f x y) 0))
(check-sat)

Dolmenls outputs:

dolmenls: The term: `y` has type `Prop` but was expected to be of type `int`

But we expect Bool instead of Prop and Int instead of int.

PS: I didn't open a new issue for such a tiny problem but I can do so if you want.

from dolmen.

Ah, that's an unfortunate problem of the current code, which uses the same type for Bool and Prop, which is correct, but lead to currently poor/confusing error messages. Ideally the solution will be to print these in the input language once we have the printers (which I should really try and get done at one point).

from dolmen.

Is there a reason for refusing to check models with an unknown status? My understanding of the SMT-LIB specification is that the solver should move to sat mode after replying unknown, and respond to get-model and co. The model is not required to be valid by the spec, but it is still interesting to be able to check if it is valid or not.

from dolmen.

No real reason, I just didn't really think about that situation.
In such a case though, what would be the expected output of dolmen when asked to verify an model that is incorrect ?

from dolmen.

Maybe display warnings rather than errors for failed assertions?

from dolmen.

That would work. I'll probably implement that soon.

from dolmen.