diff --git a/tests/benchpress.sexp b/tests/benchpress.sexp
index 9a347b4f..67b891aa 100644
--- a/tests/benchpress.sexp
+++ b/tests/benchpress.sexp
@@ -9,7 +9,7 @@
 
 (dir
   (path $cur_dir)
-  (pattern ".*.(smt2|cnf)")
+  (pattern ".*.(smt2|cnf)$")
   (expect (try (run smtlib-read-status) (run z3))))
 
 (task
diff --git a/tests/unsat/typed_v3l40070.cvc.smt2 b/tests/unsat/typed_v3l40070.cvc.smt2
new file mode 100644
index 00000000..76f8e35e
--- /dev/null
+++ b/tests/unsat/typed_v3l40070.cvc.smt2
@@ -0,0 +1,34 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_DT)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2017-04-28
+Generator: Random, converted to v2.6 by CVC4
+Application: Regressions for datatypes decision procedure.
+Target solver: CVC3
+Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "random")
+(set-info :status unsat)
+
+
+(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))
+((cons (car tree) (cdr list)) (null))
+((node (children list)) (leaf (data nat)))
+))
+(declare-fun x1 () nat)
+(declare-fun x2 () nat)
+(declare-fun x3 () nat)
+(declare-fun x4 () list)
+(declare-fun x5 () list)
+(declare-fun x6 () list)
+(declare-fun x7 () tree)
+(declare-fun x8 () tree)
+(declare-fun x9 () tree)
+
+(assert (and (and (and (not (= zero (ite ((_ is leaf) (node x4)) (data (node x4)) zero))) ((_ is node) x7)) (= x9 x8)) (not (= (ite ((_ is cons) (ite ((_ is cons) x4) (cdr x4) null)) (cdr (ite ((_ is cons) x4) (cdr x4) null)) null) null))))
+(check-sat)
+(exit)
+
+
diff --git a/tests/unsat/typed_v5l90068.cvc.smt2 b/tests/unsat/typed_v5l90068.cvc.smt2
new file mode 100644
index 00000000..4157b5f6
--- /dev/null
+++ b/tests/unsat/typed_v5l90068.cvc.smt2
@@ -0,0 +1,40 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_DT)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2017-04-28
+Generator: Random, converted to v2.6 by CVC4
+Application: Regressions for datatypes decision procedure.
+Target solver: CVC3
+Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "random")
+(set-info :status unsat)
+
+
+(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))
+((cons (car tree) (cdr list)) (null))
+((node (children list)) (leaf (data nat)))
+))
+(declare-fun x1 () nat)
+(declare-fun x2 () nat)
+(declare-fun x3 () nat)
+(declare-fun x4 () nat)
+(declare-fun x5 () nat)
+(declare-fun x6 () list)
+(declare-fun x7 () list)
+(declare-fun x8 () list)
+(declare-fun x9 () list)
+(declare-fun x10 () list)
+(declare-fun x11 () tree)
+(declare-fun x12 () tree)
+(declare-fun x13 () tree)
+(declare-fun x14 () tree)
+(declare-fun x15 () tree)
+
+(assert (and (and (and (and (and (and (and (and ((_ is node) x13) (not ((_ is succ) x1))) (= zero (succ x5))) ((_ is null) x8)) ((_ is zero) x1)) (= x11 x15)) (not (= x10 x9))) (not (= (leaf x2) x13))) (= x15 (leaf x5))))
+(check-sat)
+(exit)
+
+