Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
Halbaroth opened this issue Jul 18, 2023 · 1 comment · Fixed by #753
Closed

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

Halbaroth opened this issue Jul 18, 2023 · 1 comment · Fixed by #753
Assignees
Milestone

Comments

@Halbaroth
Copy link
Collaborator

Halbaroth commented Jul 18, 2023

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.")
@Halbaroth Halbaroth added this to the 2.5.0 milestone Jul 18, 2023
@Halbaroth Halbaroth self-assigned this Jul 18, 2023
@Halbaroth Halbaroth linked a pull request Jul 18, 2023 that will close this issue
@bclement-ocp
Copy link
Collaborator

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

bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Jul 25, 2023
Halbaroth pushed a commit that referenced this issue Jul 25, 2023
This is a reloaded version of #738 with tests.

Fixes #737
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants