From 494bf99194fa4c9eb55eaffa0d090777a34e6359 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 21 Apr 2015 09:55:11 +0200
Subject: [PATCH] Adding an example of a tester in SMT2.

---
 test/regress/regress0/datatypes/Makefile.am  | 3 ++-
 test/regress/regress0/datatypes/is_test.smt2 | 6 ++++++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/datatypes/is_test.smt2

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 88f588aa0..b323a2732 100644
--- 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
index 000000000..9c38ffcc8
--- /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)
-- 
2.30.2