diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-27 18:52:44 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-27 23:52:44 +0000 |
commit | 61321e583c889ca097b1ac008899a43467cabc21 (patch) | |
tree | de129bfbc1a29aa6d9ab6ff154b2c274fa178103 /test/regress/regress0 | |
parent | 898290ddffe61d19588182cc01a8af39c9252156 (diff) |
Add missing API checks to getValue (#7475)
Fixes cvc5/cvc5-projects#307.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/cvc-rerror-print.cvc.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/proj-issue307-get-value-re.smt2 | 7 |
2 files changed, 8 insertions, 1 deletions
diff --git a/test/regress/regress0/cvc-rerror-print.cvc.smt2 b/test/regress/regress0/cvc-rerror-print.cvc.smt2 index 03ba7c91c..d3ffb7a7e 100644 --- a/test/regress/regress0/cvc-rerror-print.cvc.smt2 +++ b/test/regress/regress0/cvc-rerror-print.cvc.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -; EXPECT: (error "Cannot get model unless after a SAT or unknown response.") +; EXPECT: (error "Cannot get model unless after a SAT or UNKNOWN response.") (set-option :incremental false) (set-logic ALL) (set-option :produce-models true) diff --git a/test/regress/regress0/proj-issue307-get-value-re.smt2 b/test/regress/regress0/proj-issue307-get-value-re.smt2 new file mode 100644 index 000000000..c52e476e0 --- /dev/null +++ b/test/regress/regress0/proj-issue307-get-value-re.smt2 @@ -0,0 +1,7 @@ +; SCRUBBER: grep -v -E '\(error' +; EXPECT: sat +(reset) +(set-logic ALL) +(set-option :produce-models true) +(check-sat) +(get-value ((re.opt re.allchar))) |