6 files changed, 60 insertions, 3 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 5eda230c3..58788c194 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -43,7 +43,8 @@ SMT2_TESTS = \
 	simple-lra.smt2 \
 	simple-rdl.smt2 \
 	simple-uf.smt2 \
-	simplification_bug4.smt2
+	simplification_bug4.smt2 \
+	parallel-let.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \
@@ -115,7 +116,10 @@ BUG_TESTS = \
 	buggy-ite.smt2 \
 	bug303.smt2 \
 	bug310.cvc \
-	bug339.smt2
+	bug322.cvc \
+	bug322b.cvc \
+	bug339.smt2 \
+	bug365.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug322.cvc b/test/regress/regress0/bug322.cvc
new file mode 100644
index 000000000..c68fde795
--- /dev/null
+++ b/test/regress/regress0/bug322.cvc
@@ -0,0 +1,23 @@
+% EXPECT: sat
+% EXIT: 10
+% Preamble  --------------
+DATATYPE UNIT = Unit END;
+DATATYPE BOOL = Truth | Falsity END;
+
+% Decls     --------------
+node$type: TYPE;
+value$type: TYPE;
+Nodes$elem$type: TYPE = node$type;
+Nodes$t$type: TYPE;
+node_pair_set$type: TYPE = ARRAY node$type OF ARRAY node$type OF BOOL;
+failure_pattern$type: TYPE = node_pair_set$type;
+is_faulty:(node$type, failure_pattern$type) -> BOOL = (LAMBDA (p: node$type, 
+                                                               deliver: failure_pattern$type): 
+                                                      (IF (EXISTS (q: node$type): 
+                                                          (NOT ((((deliver)[
+                                                                 (p)])[
+                                                                (q)]) = 
+                                                               (Truth)))) THEN 
+                                                      (Truth) ELSE (Falsity) ENDIF));
+
+CHECKSAT;
diff --git a/test/regress/regress0/bug322b.cvc b/test/regress/regress0/bug322b.cvc
new file mode 100644
index 000000000..d10292dd5
--- /dev/null
+++ b/test/regress/regress0/bug322b.cvc
@@ -0,0 +1,12 @@
+% COMMAND-LINE: --incremental
+% EXPECT: valid
+% EXPECT: valid
+% EXPECT: valid
+% EXIT: 20
+x : INT;
+y : INT = x + 1;
+z : INT = -10;
+identity : INT -> INT = LAMBDA(x:INT) : x;
+QUERY identity(x) = x;
+QUERY identity(y) > x;
+QUERY identity(z) = -10;
diff --git a/test/regress/regress0/bug365.smt2 b/test/regress/regress0/bug365.smt2
new file mode 100644
index 000000000..6dd48a849
--- /dev/null
+++ b/test/regress/regress0/bug365.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_LIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(assert (let
+	   ((a 2))
+	   (= a (let ((a 7)) a))))
+(check-sat)
+(exit)
+
diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc
index 80aecfe25..49684241c 100644
--- a/test/regress/regress0/datatypes/rec2.cvc
+++ b/test/regress/regress0/datatypes/rec2.cvc
@@ -1,7 +1,7 @@
 % EXPECT: valid
 % EXIT: 20
 c : BOOLEAN;
-a16 : [# _a : REAL, _b : REAL #] = (
+a16 : [# _a : INT, _b : INT #] = (
         IF c THEN (# _a := 3, _b := 2 #)
         ELSE (# _a := 1, _b := 5 #)
         ENDIF WITH ._a := 2);
diff --git a/test/regress/regress0/parallel-let.smt2 b/test/regress/regress0/parallel-let.smt2
new file mode 100644
index 000000000..1f12522ee
--- /dev/null
+++ b/test/regress/regress0/parallel-let.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
+(assert (distinct x y))
+(assert (let ((x y) (y x)) (= x y)))
+(check-sat)
+(exit)