diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-05 14:07:47 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-05 15:41:21 -0500 |
| commit | 7eb063762c8b1d9366cf2b4d4687019f7733411b (patch) | |
| tree | c89c4e018610c56e18b35d2835f3b200208dc27e /test/regress/regress0 | |
| parent | c0b0632a83ca1e997b9002bf9e67b0dbbbd154b1 (diff) | |
Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now works).
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/pair-bool-bool.cvc | 10 |
2 files changed, 12 insertions, 1 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 31999b203..67b97add3 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -36,6 +36,8 @@ TESTS = \ datatype13.cvc \ empty_tuprec.cvc \ mutually-recursive.cvc \ + pair-real-bool.smt2 \ + pair-bool-bool.cvc \ rewriter.cvc \ typed_v10l30054.cvc \ typed_v1l80005.cvc \ @@ -60,7 +62,6 @@ TESTS = \ wrong-sel-simp.cvc FAILING_TESTS = \ - pair-real-bool.smt2 \ datatype-dump.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/datatypes/pair-bool-bool.cvc b/test/regress/regress0/datatypes/pair-bool-bool.cvc new file mode 100644 index 000000000..7525e2dbb --- /dev/null +++ b/test/regress/regress0/datatypes/pair-bool-bool.cvc @@ -0,0 +1,10 @@ +% EXPECT: sat + +DATATYPE + pair[T1,T2] = mkpair(first:T1, second:T2) +END; + +x : pair[BOOLEAN,BOOLEAN]; + +ASSERT x = mkpair(TRUE,TRUE); +CHECKSAT; |