Skip to content

Commit

Permalink
Update tests
Browse files Browse the repository at this point in the history
  • Loading branch information
Stevendeo committed Nov 27, 2023
1 parent 5d35613 commit 7623914
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 2 deletions.
15 changes: 14 additions & 1 deletion tests/cram.t/run.t
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,20 @@ And some SMT2 action.
Here are some tests to check that we have sane behavior given the insane
combinations of produce-models et al.

First, if model generation is not enabled, we should error out when a
First, if (get-model) is called outside the SAT mode, we should fail.
$ echo '(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
(error "Invalid action during mode Start: Command get-model")


$ echo '(set-logic ALL)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
(error "Invalid action during mode Assert: Command get-model")

$ echo '(set-logic ALL)(assert false)(check-sat)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null

unsat
(error "Invalid action during mode Unsat: Command get-model")

Then, if model generation is not enabled, we should error out when a
`(get-model)` statement is issued:

$ echo '(set-logic ALL)(check-sat)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
Expand Down
2 changes: 1 addition & 1 deletion tests/smtlib/testfile-steps-bound1.dolmen.err.expected
Original file line number Diff line number Diff line change
@@ -1 +1 @@
(error "Invalid action during mode Util.Assert: Set option steps_bound")
(error "Invalid action during mode Assert: Set option steps_bound")

0 comments on commit 7623914

Please sign in to comment.