From e4fde716f0b8266412cb6dc6326642c718839b71 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 16 Mar 2017 14:19:58 -0500 Subject: More fixes, features to examples. --- test/regress/regress0/datatypes/dt-color-2.6.smt2 | 4 +++- test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 | 10 ++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) (limited to 'test/regress') 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) -- cgit v1.2.3