diff options
Diffstat (limited to 'test')
-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; |