Unclear error message during model checking

[Halbaroth]

I was using Dolmen to check models generated by Alt-Ergo as follow:
alt-ergo --produce-models --frontend dolmen test.smt2 | dolmen --check-model true test.smt2
and I got the message:

File "<stdin>", line 2, character 0-7:
Error while parsing an input statement, read the symbol 'unknown',
      but expected an opening parenthesis to start a command.

It makes sense that Dolmen refuses this response file since AE gives a model but outputs unknown. If I replace the answer by sat, everything works but the error message is not very clear.

Besides, why do you use a boolean value for the option --check-model? In my opinion a flag would be better.

[Gbury]

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.

[Halbaroth]

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.

[Gbury]

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).

[bclement-ocp]

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.

[Gbury]

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 ?

[bclement-ocp]

Maybe display warnings rather than errors for failed assertions?

[Gbury]

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