diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-20 18:05:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-20 18:05:43 -0500 |
| commit | a0c5a51f6fae81ffeb1752ee4d75db7a51c23680 (patch) | |
| tree | 9f592a260c1dfe2cd311b0668ba6bd0ecd8d0713 /test/regress/regress0 | |
| parent | 34a4f78458773e9816d90c84fd2047b74a699527 (diff) | |
Add regressions that increase coverage (#2337)
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/datatypes/data-nested-codata.smt2 | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress0/datatypes/data-nested-codata.smt2 b/test/regress/regress0/datatypes/data-nested-codata.smt2 new file mode 100644 index 000000000..159ae4ae9 --- /dev/null +++ b/test/regress/regress0/datatypes/data-nested-codata.smt2 @@ -0,0 +1,21 @@ + +(set-logic QF_DTLIA) +(set-info :status sat) + +(declare-datatype List ((cons (head Int) (tail List)) (nil))) + +(declare-codatatype Stream ((mkStream (shead List) (stail Stream)))) + + +(declare-fun x () Stream) +(assert (not (is-nil (shead x)))) +(assert (not (is-nil (tail (shead x))))) +(declare-fun y () Stream) +(assert (not (is-nil (shead y)))) +(assert (not (is-nil (tail (shead y))))) +(declare-fun z () Stream) +(assert (not (is-nil (shead z)))) +(assert (not (is-nil (tail (shead z))))) +(assert (distinct x y z)) + +(check-sat) |