diff --git a/tests/sat/v1l60008.cvc.smt2 b/tests/sat/v1l60008.cvc.smt2
new file mode 100644
index 00000000..3377d60f
--- /dev/null
+++ b/tests/sat/v1l60008.cvc.smt2
@@ -0,0 +1,28 @@
+(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 sat)
+
+
+(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 () list)
+(declare-fun x3 () tree)
+
+(assert (and (and (and (and (and (not (= (cdr x2) null)) (= (children (leaf zero)) (children x3))) (not ((_ is zero) (succ x1)))) ((_ is zero) zero)) ((_ is zero) (pred (succ (data (car null)))))) (= (leaf (succ (data (car (cdr (cdr (cdr (cdr (cdr (cdr x2)))))))))) (car (cdr null)))))
+(check-sat)
+(exit)
+
+