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)