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 | |
| parent | 898290ddffe61d19588182cc01a8af39c9252156 (diff) | |
Add missing API checks to getValue (#7475)
Fixes cvc5/cvc5-projects#307.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -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 |
3 files changed, 9 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a3fd70683..2529a8622 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -856,6 +856,7 @@ set(regress_0_tests regress0/printer/let_shadowing.smt2 regress0/printer/symbol_starting_w_digit.smt2 regress0/printer/tuples_and_records.cvc.smt2 + regress0/proj-issue307-get-value-re.smt2 regress0/proofs/cyclic-ucp.smt2 regress0/proofs/issue277-circuit-propagator.smt2 regress0/proofs/lfsc-test-1.smt2 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))) |