OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
131 stars 33 forks source link

Print irrelevant smt error when we don't choose the tableaux solver #737

Closed Halbaroth closed 1 year ago

Halbaroth commented 1 year ago

Using the same input file as in the issue #719, we got the following output after running:

$ alt-ergo --frontend dolmen 719.smt2
; [Warning] File "tests/issues/719.smt2", line 2, characters 1-34: The generation of models is not supported for the current SAT solver. Please choose the SAT solver Tableaux.

; File "tests/issues/719.smt2", line 17, characters 1-12: Valid (0.5142) (38 steps) (goal g_1)

unsat
(error "You have to set the flag :produce-models with (set-option :produce-models true) before using the statement (get-model).")

We should display something like

(error "The generation of model is not supported with the current SAT solver.")
bclement-ocp commented 1 year ago

Actually the message should probably mention --produce-models rather than :produce-models.