From c55e7a613b26c7cb136912c01af04c8fc1b16f11 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 1 Dec 2019 17:38:24 -0600
Subject: [PATCH] test: add some basic datatype tests

---
 tests/unsat/data_acycl1.smt2   |  8 ++++++++
 tests/unsat/data_acycl_if.smt2 | 14 ++++++++++++++
 tests/unsat/data_card1.smt2    | 11 +++++++++++
 3 files changed, 33 insertions(+)
 create mode 100644 tests/unsat/data_acycl1.smt2
 create mode 100644 tests/unsat/data_acycl_if.smt2
 create mode 100644 tests/unsat/data_card1.smt2

diff --git a/tests/unsat/data_acycl1.smt2 b/tests/unsat/data_acycl1.smt2
new file mode 100644
index 00000000..f5505cc7
--- /dev/null
+++ b/tests/unsat/data_acycl1.smt2
@@ -0,0 +1,8 @@
+
+(set-info :status unsat)
+(declare-datatypes ((nat 0)) (((Z) (S (pred nat)))))
+(declare-const n nat)
+
+(assert (= n (S (S n))))
+
+(check-sat)
diff --git a/tests/unsat/data_acycl_if.smt2 b/tests/unsat/data_acycl_if.smt2
new file mode 100644
index 00000000..2d25a0d5
--- /dev/null
+++ b/tests/unsat/data_acycl_if.smt2
@@ -0,0 +1,14 @@
+
+(set-info :status unsat)
+(declare-datatypes ((nat 0)) (((Z) (S (pred nat)))))
+(declare-const p Bool)
+(declare-const n nat)
+(declare-const n_t nat)
+(declare-const n_f nat)
+
+(assert (= n_t (S n)))
+(assert (= n_f (S (S n))))
+(assert (=> p (= n (S n_t))))
+(assert (=> (not p) (= n (S n_f))))
+
+(check-sat)
diff --git a/tests/unsat/data_card1.smt2 b/tests/unsat/data_card1.smt2
new file mode 100644
index 00000000..758891ef
--- /dev/null
+++ b/tests/unsat/data_card1.smt2
@@ -0,0 +1,11 @@
+
+(set-info :status unsat)
+(declare-datatypes ((three 0)) (((A) (B) (C))))
+(declare-const t1 three)
+(declare-const t2 three)
+(declare-const t3 three)
+(declare-const t4 three)
+
+(assert (distinct t1 t2 t3 t4))
+
+(check-sat)