Adding an example of a tester in SMT2.

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 88f588aa00d59781667bfa8213878f5fd089c378..b323a27328b7220c1866daf6e7477a9813a75e55 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -62,7 +62,8 @@ TESTS =       \
        wrong-sel-simp.cvc \
        tenum-bug.smt2 \
        cdt-non-canon-stream.smt2 \
-       stream-singleton.smt2
+       stream-singleton.smt2 \
+       is_test.smt2
 
 FAILING_TESTS = \
        datatype-dump.cvc

diff --git a/test/regress/regress0/datatypes/is_test.smt2 b/test/regress/regress0/datatypes/is_test.smt2
new file mode 100644 (file)
index 0000000..9c38ffc
--- /dev/null
+++ b/test/regress/regress0/datatypes/is_test.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((Unit (u))))
+(declare-fun x () Unit)
+(assert (not (is-u x)))
+(check-sat)