diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 14:19:58 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 14:19:58 -0500 |
| commit | e4fde716f0b8266412cb6dc6326642c718839b71 (patch) | |
| tree | 092819d4bf1c0d26f845a3393a6462937280a02c /test | |
| parent | 00785f2b65eb9dfdfbfcd8b58b0cc57255919c31 (diff) | |
More fixes, features to examples.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/datatypes/dt-color-2.6.smt2 | 4 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 | 10 |
2 files changed, 13 insertions, 1 deletions
diff --git a/test/regress/regress0/datatypes/dt-color-2.6.smt2 b/test/regress/regress0/datatypes/dt-color-2.6.smt2 index a44219954..f6148994e 100644 --- a/test/regress/regress0/datatypes/dt-color-2.6.smt2 +++ b/test/regress/regress0/datatypes/dt-color-2.6.smt2 @@ -10,6 +10,8 @@ (declare-fun d () Color) (assert (or (distinct a b c d) - (< (match a ((red 5) (green 3) (blue 2))) 0))) + (< (match a ((red 5) (green 3) (blue 2))) 0) + (< (match b ((red 2) (_ 1))) 0) + )) (check-sat) diff --git a/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 b/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 index e2f4a779b..430b22c59 100644 --- a/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 +++ b/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 @@ -11,4 +11,14 @@ (declare-fun t () TreeList) (assert (<= 100 (match t ((empty (- 1)) ((insert x1 x2) (value x1)))))) + +(declare-datatypes ( ( PTree 1) ( PTreeList 1) ) ( +(par ( X ) ( ( pnode ( pvalue X ) ( pchildren ( PTreeList X )) ))) +(par ( Y ) ( ( pempty ) ( pinsert ( phead ( PTree Y )) ( ptail ( PTreeList Y ))) )) +)) + +(declare-fun pt () (PTreeList Int)) +(assert (<= 200 (match pt ((pempty (- 1)) ((pinsert x1 x2) (pvalue x1)))))) + + (check-sat) |