5 files changed, 39 insertions, 2 deletions
diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
index 96b5d2928..fe02b230e 100644
--- a/test/regress/regress0/preprocess/Makefile.am
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -37,7 +37,10 @@ CVC_TESTS = \
 	preprocess_09.cvc \
 	preprocess_10.cvc \
 	preprocess_11.cvc \
-	preprocess_12.cvc
+	preprocess_12.cvc \
+	preprocess_13.cvc \
+	preprocess_14.cvc \
+	preprocess_15.cvc
 
 # Regression tests derived from bug reports
 BUG_TESTS = 
diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc b/test/regress/regress0/preprocess/preprocess_13.cvc
new file mode 100644
index 000000000..7a2ed7dd8
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_13.cvc
@@ -0,0 +1,10 @@
+% EXPECT: valid
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+QUERY (a0 OR (a1 OR (a2 OR (a3 OR (a4 OR (a5 OR (FALSE OR (a6 OR (a7 OR (a8 OR a9))))))))));
+
+% EXIT: 20
+
diff --git a/test/regress/regress0/preprocess/preprocess_14.cvc b/test/regress/regress0/preprocess/preprocess_14.cvc
new file mode 100644
index 000000000..04a6f4c50
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_14.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a6 AND (a7 AND (a8 AND a9))))))))));
+
+CHECKSAT;
+
+% EXIT: 10
+
diff --git a/test/regress/regress0/preprocess/preprocess_15.cvc b/test/regress/regress0/preprocess/preprocess_15.cvc
new file mode 100644
index 000000000..30df35e53
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_15.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a3 AND (a6 AND (a7 AND (a8 AND a9)))))))))));
+
+CHECKSAT;
+
+% EXIT: 10
+
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index e71dcb41d..ccba0164a 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -55,7 +55,7 @@ public:
     d_addClauseCalled(false) {
   }
 
-  SatVariable newVar(bool theoryAtom) {
+  SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) {
     return d_nextVar++;
   }