Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

14 files changed, 599 insertions, 10 deletions

diff --git a/test/Makefile.am b/test/Makefile.am
index 4f7818ade..2bcb283d7 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -35,6 +35,7 @@ subdirs_to_check = \
 	regress/regress0/arith/integers \
 	regress/regress0/uf \
 	regress/regress0/uflra \
+	regress/regress0/uflia \
 	regress/regress0/bv \
 	regress/regress0/bv/core \
 	regress/regress0/arrays \
@@ -43,6 +44,7 @@ subdirs_to_check = \
 	regress/regress0/push-pop \
 	regress/regress0/precedence \
 	regress/regress0/preprocess \
+	regress/regress0/subtypes \
 	regress/regress1 \
 	regress/regress2 \
 	regress/regress3
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 1c4071c00..016bf6e2a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -41,7 +41,8 @@ SMT2_TESTS = \
 	ite4.smt2 \
 	simple-lra.smt2 \
 	simple-rdl.smt2 \
-	simple-uf.smt2
+	simple-uf.smt2 \
+	simplification_bug4.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \
@@ -105,7 +106,8 @@ EXTRA_DIST = $(TESTS) \
 	bug216.smt2.expect \
 	bug288b.smt \
 	bug288c.smt \
-	bug288.smt
+	bug288.smt \
+	simplification_bug4.smt2.expect
 
 if CVC4_BUILD_PROFILE_COMPETITION
 else
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index c4a4e2fdd..581897535 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -12,6 +12,10 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
+	tuple.cvc \
+	rec1.cvc \
+	rec2.cvc \
+	rec5.cvc \
 	datatype.cvc \
 	datatype0.cvc \
 	datatype1.cvc \
@@ -45,7 +49,8 @@ endif
 
 # and make sure to distribute it
 EXTRA_DIST += \
-	error.cvc
+	error.cvc \
+	rec4.cvc
 
 # synonyms for "check"
 .PHONY: regress regress0 test
diff --git a/test/regress/regress0/datatypes/rec1.cvc b/test/regress/regress0/datatypes/rec1.cvc
new file mode 100644
index 000000000..25e14eac0
--- /dev/null
+++ b/test/regress/regress0/datatypes/rec1.cvc
@@ -0,0 +1,8 @@
+% EXPECT: valid
+% EXIT: 20
+c : BOOLEAN;
+a17 : BOOLEAN = ((# _a := 2, _b := 2 #) = (
+          IF c THEN (# _a := 3, _b := 2 #)
+          ELSE (# _a := 1, _b := 2 #)
+          ENDIF WITH ._a := 2));
+QUERY a17;
diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc
new file mode 100644
index 000000000..80aecfe25
--- /dev/null
+++ b/test/regress/regress0/datatypes/rec2.cvc
@@ -0,0 +1,12 @@
+% EXPECT: valid
+% EXIT: 20
+c : BOOLEAN;
+a16 : [# _a : REAL, _b : REAL #] = (
+        IF c THEN (# _a := 3, _b := 2 #)
+        ELSE (# _a := 1, _b := 5 #)
+        ENDIF WITH ._a := 2);
+a21 : BOOLEAN = 
+        IF c THEN ((# _a := 2, _b := 2 #) = a16)
+        ELSE ((# _a := 2, _b := 5 #) = a16)
+        ENDIF;
+QUERY a21;
diff --git a/test/regress/regress0/datatypes/rec4.cvc b/test/regress/regress0/datatypes/rec4.cvc
new file mode 100644
index 000000000..c474502d5
--- /dev/null
+++ b/test/regress/regress0/datatypes/rec4.cvc
@@ -0,0 +1,11 @@
+% EXPECT: valid
+% EXIT: 20
+a : BOOLEAN;
+a49 : BOOLEAN = (
+          IF a THEN (# _a := 1 #)
+          ELSE (# _a := 2 #)
+          ENDIF = (# _a := 
+          IF a THEN 1
+          ELSE 2
+          ENDIF #));
+QUERY a49;
diff --git a/test/regress/regress0/datatypes/rec5.cvc b/test/regress/regress0/datatypes/rec5.cvc
new file mode 100644
index 000000000..d52174b8e
--- /dev/null
+++ b/test/regress/regress0/datatypes/rec5.cvc
@@ -0,0 +1,205 @@
+% EXPECT: invalid
+% EXIT: 10
+bit__ty: TYPE = [0..1];
+bc1553__lru_name: TYPE = [0..11];
+bus__inputs__type: TYPE;
+bus__word_index: TYPE = INT;
+cartesian__position: TYPE = [# x: INT, y: INT, z: INT #];
+ibit__phase: TYPE = [0..6];
+measuretypes__meter: TYPE = INT;
+bc1553__asi: [0..11];
+bc1553__barometer: [0..11];
+bc1553__compass: [0..11];
+bc1553__destruct: [0..11];
+bc1553__fins: [0..11];
+bc1553__fuel: [0..11];
+bc1553__fuze: [0..11];
+bc1553__infrared: [0..11];
+bc1553__ins: [0..11];
+bc1553__lru_name__base__first: [0..11];
+bc1553__lru_name__base__last: [0..11];
+bc1553__lru_name__first: [0..11];
+bc1553__lru_name__last: [0..11];
+bc1553__lru_name__size: INT;
+bc1553__motor: [0..11];
+bc1553__radar: [0..11];
+bc1553__warhead: [0..11];
+bus__all_msg_index__base__first: INT;
+bus__all_msg_index__base__last: INT;
+bus__all_msg_index__first: INT;
+bus__all_msg_index__last: INT;
+bus__all_msg_index__size: INT;
+bus__lru_subaddress_index__base__first: INT;
+bus__lru_subaddress_index__base__last: INT;
+bus__lru_subaddress_index__first: INT;
+bus__lru_subaddress_index__last: INT;
+bus__lru_subaddress_index__size: INT;
+bus__word__base__first: INT;
+bus__word__base__last: INT;
+bus__word__first: INT;
+bus__word__last: INT;
+bus__word__size: INT;
+bus__word_index__base__first: INT;
+bus__word_index__base__last: INT;
+bus__word_index__first: INT;
+bus__word_index__last: INT;
+bus__word_index__size: INT;
+bus_id: [0..11];
+ibit__fail: [0..6];
+ibit__in_progress: [0..6];
+ibit__off: [0..6];
+ibit__pass: [0..6];
+ibit__phase__base__first: [0..6];
+ibit__phase__base__last: [0..6];
+ibit__phase__first: [0..6];
+ibit__phase__last: [0..6];
+ibit__phase__size: INT;
+ibit__request_start: [0..6];
+ibit__request_stop: [0..6];
+ibit__timeout: [0..6];
+integer__base__first: INT;
+integer__base__last: INT;
+integer__first: INT;
+integer__last: INT;
+integer__size: INT;
+measuretypes__meter__base__first: INT;
+measuretypes__meter__base__last: INT;
+measuretypes__meter__first: INT;
+measuretypes__meter__last: INT;
+measuretypes__meter__size: INT;
+systemtypes__unsigned16__base__first: INT;
+systemtypes__unsigned16__base__last: INT;
+systemtypes__unsigned16__first: INT;
+systemtypes__unsigned16__last: INT;
+systemtypes__unsigned16__size: INT;
+bus__inputs: bus__inputs__type;
+bus__inputs__tilde: bus__inputs__type;
+ibit_request: [0..6];
+ibit_request__5: [0..6];
+ibit_request__5__tilde: [0..6];
+ibit_request__tilde: [0..6];
+last_position: [# x: INT, y: INT, z: INT #];
+last_position__1: [# x: INT, y: INT, z: INT #];
+last_position__1__tilde: [# x: INT, y: INT, z: INT #];
+last_position__2: [# x: INT, y: INT, z: INT #];
+last_position__2__tilde: [# x: INT, y: INT, z: INT #];
+last_position__3: [# x: INT, y: INT, z: INT #];
+last_position__3__tilde: [# x: INT, y: INT, z: INT #];
+last_position__tilde: [# x: INT, y: INT, z: INT #];
+word: INT;
+word__4: INT;
+word__4__tilde: INT;
+word__tilde: INT;
+bc1553__is_fresh: ([0..11], INT, bus__inputs__type) ->  BOOLEAN;
+bc1553__is_valid: ([0..11], INT, bus__inputs__type) ->  BOOLEAN;
+bc1553__lru_name__LE: ([0..11], [0..11]) ->  BOOLEAN;
+bc1553__lru_name__pos: [0..11] ->  INT;
+bc1553__lru_name__pred: [0..11] ->  [0..11];
+bc1553__lru_name__succ: [0..11] ->  [0..11];
+bc1553__lru_name__val: INT ->  [0..11];
+character__pos: INT ->  INT;
+character__val: INT ->  INT;
+ibit__phase__LE: ([0..6], [0..6]) ->  BOOLEAN;
+ibit__phase__pos: [0..6] ->  INT;
+ibit__phase__pred: [0..6] ->  [0..6];
+ibit__phase__succ: [0..6] ->  [0..6];
+ibit__phase__val: INT ->  [0..6];
+integer__pred: INT ->  INT;
+integer__succ: INT ->  INT;
+round__: REAL ->  INT;
+int__div: (INT, INT) ->  INT;
+int__mod: (INT, INT) ->  INT;
+ASSERT (bus_id = bc1553__ins);
+ASSERT (0 <= integer__size);
+ASSERT (integer__first = -(2147483647));
+ASSERT (integer__last = 2147483647);
+ASSERT (integer__base__first = -(2147483647));
+ASSERT (integer__base__last = 2147483647);
+ASSERT (0 <= systemtypes__unsigned16__size);
+ASSERT (systemtypes__unsigned16__first = 0);
+ASSERT (systemtypes__unsigned16__last = 65535);
+ASSERT (systemtypes__unsigned16__base__first = -(2147483647));
+ASSERT (systemtypes__unsigned16__base__last = 2147483647);
+ASSERT (0 <= measuretypes__meter__size);
+ASSERT (measuretypes__meter__first = -(200000));
+ASSERT (measuretypes__meter__last = 200000);
+ASSERT (measuretypes__meter__base__first = -(2147483647));
+ASSERT (measuretypes__meter__base__last = 2147483647);
+ASSERT (0 <= bus__word_index__size);
+ASSERT (bus__word_index__first = 1);
+ASSERT (bus__word_index__last = 31);
+ASSERT (bus__word_index__base__first <= bus__word_index__base__last);
+ASSERT (bus__word_index__base__first <= bus__word_index__first);
+ASSERT (bus__word_index__last <= bus__word_index__base__last);
+ASSERT (0 <= bus__word__size);
+ASSERT (bus__word__first = 0);
+ASSERT (bus__word__last = 65535);
+ASSERT (bus__word__base__first = -(2147483647));
+ASSERT (bus__word__base__last = 2147483647);
+ASSERT (0 <= bus__all_msg_index__size);
+ASSERT (bus__all_msg_index__first = 0);
+ASSERT (bus__all_msg_index__last = 63);
+ASSERT (bus__all_msg_index__base__first = -(32768));
+ASSERT (bus__all_msg_index__base__last = 32767);
+ASSERT (0 <= bus__lru_subaddress_index__size);
+ASSERT (bus__lru_subaddress_index__first = 1);
+ASSERT (bus__lru_subaddress_index__last = 8);
+ASSERT (bus__lru_subaddress_index__base__first = -(32768));
+ASSERT (bus__lru_subaddress_index__base__last = 32767);
+ASSERT (0 <= bc1553__lru_name__size);
+ASSERT (bc1553__lru_name__first = bc1553__barometer);
+ASSERT (bc1553__lru_name__last = bc1553__warhead);
+ASSERT (bc1553__lru_name__base__first = bc1553__barometer);
+ASSERT (bc1553__lru_name__base__last = bc1553__warhead);
+ASSERT (0 <= ibit__phase__size);
+ASSERT (ibit__phase__first = ibit__off);
+ASSERT (ibit__phase__last = ibit__timeout);
+ASSERT (ibit__phase__base__first = ibit__off);
+ASSERT (ibit__phase__base__last = ibit__timeout);
+ASSERT (bc1553__barometer = 0);
+ASSERT (bc1553__asi = 1);
+ASSERT (bc1553__ins = 2);
+ASSERT (bc1553__compass = 3);
+ASSERT (bc1553__fuel = 4);
+ASSERT (bc1553__fuze = 5);
+ASSERT (bc1553__radar = 6);
+ASSERT (bc1553__infrared = 7);
+ASSERT (bc1553__fins = 8);
+ASSERT (bc1553__motor = 9);
+ASSERT (bc1553__destruct = 10);
+ASSERT (bc1553__warhead = 11);
+ASSERT (ibit__off = 0);
+ASSERT (ibit__request_start = 1);
+ASSERT (ibit__in_progress = 2);
+ASSERT (ibit__request_stop = 3);
+ASSERT (ibit__pass = 4);
+ASSERT (ibit__fail = 5);
+ASSERT (ibit__timeout = 6);
+ASSERT TRUE;
+ASSERT (measuretypes__meter__first <= (last_position).z);
+ASSERT ((last_position).z <= measuretypes__meter__last);
+ASSERT (measuretypes__meter__first <= (last_position).y);
+ASSERT ((last_position).y <= measuretypes__meter__last);
+ASSERT (measuretypes__meter__first <= (last_position).x);
+ASSERT ((last_position).x <= measuretypes__meter__last);
+ASSERT TRUE;
+ASSERT (ibit__phase__first <= ibit_request);
+ASSERT (ibit_request <= ibit__phase__last);
+ASSERT (bus__lru_subaddress_index__first <= 1);
+ASSERT (1 <= bus__lru_subaddress_index__last);
+ASSERT (bc1553__lru_name__first <= bus_id);
+ASSERT (bus_id <= bc1553__lru_name__last);
+ASSERT TRUE;
+ASSERT (bc1553__is_valid(bus_id, 1, bus__inputs) => ((bus__lru_subaddress_index__first <= 1) AND (1 <= bus__lru_subaddress_index__last)));
+ASSERT (bc1553__is_valid(bus_id, 1, bus__inputs) => ((bc1553__lru_name__first <= bus_id) AND (bus_id <= bc1553__lru_name__last)));
+ASSERT (bc1553__is_valid(bus_id, 1, bus__inputs) => TRUE);
+ASSERT bc1553__is_valid(bus_id, 1, bus__inputs);
+ASSERT bc1553__is_fresh(bus_id, 1, bus__inputs);
+ASSERT (bus__word_index__first <= 2);
+ASSERT (2 <= bus__word_index__last);
+ASSERT (bus__word_index__first <= 1);
+ASSERT (1 <= bus__word_index__last);
+ASSERT (measuretypes__meter__first <= (last_position__1).x);
+ASSERT ((last_position__1).x <= measuretypes__meter__last);
+ASSERT ((last_position__1).y = (last_position).y);
+QUERY (last_position = last_position__1);
diff --git a/test/regress/regress0/datatypes/tuple.cvc b/test/regress/regress0/datatypes/tuple.cvc
new file mode 100644
index 000000000..1def5d14e
--- /dev/null
+++ b/test/regress/regress0/datatypes/tuple.cvc
@@ -0,0 +1,11 @@
+% EXPECT: valid
+% EXIT: 20
+x: [REAL,INT,REAL] = ( 4/5, 9, 11/9 );
+first_elem: REAL = x.0;
+third_elem: REAL = x.2;
+
+Tup: TYPE = [REAL,INT,REAL];
+y:  Tup = ( 4/5, 9, 11/9 );
+y1: Tup = y WITH .1 := 3; 
+
+QUERY x=y AND first_elem = y1.0 AND third_elem = y1.2 AND y1.1 = 3;
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index aedf03470..f43a4d183 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -20,6 +20,9 @@ CVC_TESTS = \
 	units.cvc \
 	incremental-subst-bug.cvc
 
+SMT2_TESTS = \
+	tiny_bug.smt2
+
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) 
diff --git a/test/regress/regress0/push-pop/tiny_bug.smt2 b/test/regress/regress0/push-pop/tiny_bug.smt2
new file mode 100644
index 000000000..83ccca49e
--- /dev/null
+++ b/test/regress/regress0/push-pop/tiny_bug.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --incremental --simplification=none
+; EXPECT: sat
+; EXPECT: unsat
+; EXIT: 20
+(set-logic QF_UFLIA)
+(declare-fun base () Int)
+(declare-fun n () Int)
+
+(declare-fun g (Int) Bool)
+(declare-fun f (Int) Bool)
+
+(push 1)
+(assert (<= 0 n))
+(assert (f n))
+(assert (= (f n) (or (= (- n base) 1) (g n))))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (<= 0 n))
+
+(assert (or (= (- n base) 1) (g n)))
+(assert (not (g n)))
+(assert (= base (- 2)))
+
+(check-sat)
+(pop 1)
+
diff --git a/test/regress/regress0/simplification_bug4.smt2 b/test/regress/regress0/simplification_bug4.smt2
new file mode 100644
index 000000000..0d62d6921
--- /dev/null
+++ b/test/regress/regress0/simplification_bug4.smt2
@@ -0,0 +1,295 @@
+(set-logic QF_LIA)
+;; Simplified benchmark, derived from NuSMV output durationThm_1.bmc_k100.smt2
+;;
+;; Original version generated by Alberto Griggio <griggio@fbk.eu>
+;; on Fri Feb  4 15:56:12 2011
+(declare-fun sb_0__AT0 () Bool)
+(declare-fun si_0__AT0 () Int)
+(declare-fun si_1__AT0 () Int)
+(declare-fun sb_1__AT0 () Bool)
+(declare-fun si_2__AT0 () Int)
+(declare-fun si_3__AT0 () Int)
+(declare-fun sb_2__AT0 () Bool)
+(declare-fun si_4__AT0 () Int)
+(declare-fun si_5__AT0 () Int)
+(declare-fun sb_3__AT0 () Bool)
+(declare-fun sb_4__AT0 () Bool)
+(declare-fun sb_5__AT0 () Bool)
+(declare-fun si_6__AT0 () Int)
+(declare-fun si_7__AT0 () Int)
+(declare-fun si_8__AT0 () Int)
+(declare-fun si_9__AT0 () Int)
+(declare-fun si_10__AT0 () Int)
+(declare-fun si_11__AT0 () Int)
+(declare-fun sb_6__AT0 () Bool)
+(declare-fun sb_7__AT0 () Bool)
+(declare-fun si_12__AT0 () Int)
+(declare-fun si_13__AT0 () Int)
+(declare-fun si_14__AT0 () Int)
+(assert (let ((.def_61 (= si_2__AT0 si_4__AT0)))
+(let ((.def_60 (= si_3__AT0 si_5__AT0)))
+(let ((.def_62 (and .def_60 .def_61)))
+(let ((.def_63 (and sb_2__AT0 .def_62)))
+(let ((.def_59 (= si_8__AT0 0)))
+(let ((.def_64 (and .def_59 .def_63)))
+(let ((.def_58 (= si_11__AT0 0)))
+(let ((.def_65 (and .def_58 .def_64)))
+(let ((.def_53 (<= 1 si_0__AT0)))
+(let ((.def_52 (<= 1 si_1__AT0)))
+(let ((.def_54 (and .def_52 .def_53)))
+(let ((.def_48 (<= si_0__AT0 si_6__AT0)))
+(let ((.def_49 (not .def_48)))
+(let ((.def_50 (or sb_4__AT0 .def_49)))
+(let ((.def_55 (and .def_50 .def_54)))
+(let ((.def_45 (<= si_1__AT0 si_9__AT0)))
+(let ((.def_46 (not .def_45)))
+(let ((.def_47 (or sb_5__AT0 .def_46)))
+(let ((.def_56 (and .def_47 .def_55)))
+(let ((.def_57 (= sb_7__AT0 .def_56)))
+(let ((.def_66 (and .def_57 .def_65)))
+(let ((.def_44 (= si_14__AT0 0)))
+(let ((.def_67 (and .def_44 .def_66)))
+(let ((.def_33 (not sb_1__AT0)))
+(let ((.def_34 (or sb_2__AT0 .def_33)))
+(let ((.def_35 (= sb_0__AT0 .def_34)))
+(let ((.def_32 (= si_0__AT0 si_2__AT0)))
+(let ((.def_36 (and .def_32 .def_35)))
+(let ((.def_31 (= si_1__AT0 si_3__AT0)))
+(let ((.def_37 (and .def_31 .def_36)))
+(let ((.def_30 (= sb_1__AT0 sb_6__AT0)))
+(let ((.def_38 (and .def_30 .def_37)))
+(let ((.def_29 (= si_6__AT0 si_8__AT0)))
+(let ((.def_39 (and .def_29 .def_38)))
+(let ((.def_28 (= si_9__AT0 si_11__AT0)))
+(let ((.def_40 (and .def_28 .def_39)))
+(let ((.def_27 (= sb_6__AT0 sb_7__AT0)))
+(let ((.def_41 (and .def_27 .def_40)))
+(let ((.def_26 (= si_12__AT0 si_14__AT0)))
+(let ((.def_42 (and .def_26 .def_41)))
+(let ((.def_68 (and .def_42 .def_67)))
+.def_68
+))))))))))))))))))))))))))))))))))))))))))
+
+; (push 1)
+; (assert (let ((.def_69 (not sb_0__AT0)))
+; .def_69
+; ))
+; (check-sat)
+; (pop 1)
+
+(declare-fun sb_0__AT1 () Bool)
+(declare-fun si_0__AT1 () Int)
+(declare-fun si_1__AT1 () Int)
+(declare-fun sb_1__AT1 () Bool)
+(declare-fun si_2__AT1 () Int)
+(declare-fun si_3__AT1 () Int)
+(declare-fun sb_2__AT1 () Bool)
+(declare-fun si_4__AT1 () Int)
+(declare-fun si_5__AT1 () Int)
+(declare-fun sb_3__AT1 () Bool)
+(declare-fun sb_4__AT1 () Bool)
+(declare-fun sb_5__AT1 () Bool)
+(declare-fun si_6__AT1 () Int)
+(declare-fun si_7__AT1 () Int)
+(declare-fun si_8__AT1 () Int)
+(declare-fun si_9__AT1 () Int)
+(declare-fun si_10__AT1 () Int)
+(declare-fun si_11__AT1 () Int)
+(declare-fun sb_6__AT1 () Bool)
+(declare-fun sb_7__AT1 () Bool)
+(declare-fun si_12__AT1 () Int)
+(declare-fun si_13__AT1 () Int)
+(declare-fun si_14__AT1 () Int)
+(assert (let ((.def_163 (= si_0__AT0 si_2__AT1)))
+(let ((.def_162 (= si_1__AT0 si_3__AT1)))
+(let ((.def_164 (and .def_162 .def_163)))
+(let ((.def_155 (* (- 1) si_12__AT1)))
+(let ((.def_156 (+ si_1__AT1 .def_155)))
+(let ((.def_157 (+ si_0__AT1 .def_156)))
+(let ((.def_158 (<= .def_157 0)))
+(let ((.def_159 (not .def_158)))
+(let ((.def_160 (or sb_5__AT1 .def_159)))
+(let ((.def_161 (= sb_2__AT1 .def_160)))
+(let ((.def_165 (and .def_161 .def_164)))
+(let ((.def_147 (* (- 1) si_7__AT1)))
+(let ((.def_148 (+ si_6__AT0 .def_147)))
+(let ((.def_149 (= .def_148 (- 1))))
+(let ((.def_142 (not sb_3__AT0)))
+(let ((.def_150 (or .def_142 .def_149)))
+(let ((.def_144 (= si_7__AT1 0)))
+(let ((.def_145 (or sb_3__AT0 .def_144)))
+(let ((.def_151 (and .def_145 .def_150)))
+(let ((.def_139 (* (- 1) si_13__AT1)))
+(let ((.def_140 (+ si_12__AT0 .def_139)))
+(let ((.def_141 (= .def_140 (- 1))))
+(let ((.def_143 (or .def_141 .def_142)))
+(let ((.def_152 (and .def_143 .def_151)))
+(let ((.def_136 (= si_13__AT1 0)))
+(let ((.def_137 (or sb_3__AT0 .def_136)))
+(let ((.def_153 (and .def_137 .def_152)))
+(let ((.def_166 (and .def_153 .def_165)))
+(let ((.def_133 (not sb_4__AT0)))
+(let ((.def_130 (* (- 1) si_10__AT1)))
+(let ((.def_131 (+ si_9__AT0 .def_130)))
+(let ((.def_132 (= .def_131 (- 1))))
+(let ((.def_134 (or .def_132 .def_133)))
+(let ((.def_126 (= si_10__AT1 0)))
+(let ((.def_127 (or sb_4__AT0 .def_126)))
+(let ((.def_135 (and .def_127 .def_134)))
+(let ((.def_167 (and .def_135 .def_166)))
+(let ((.def_125 (= si_7__AT1 si_8__AT1)))
+(let ((.def_168 (and .def_125 .def_167)))
+(let ((.def_124 (= si_10__AT1 si_11__AT1)))
+(let ((.def_169 (and .def_124 .def_168)))
+(let ((.def_118 (<= 1 si_0__AT1)))
+(let ((.def_117 (<= 1 si_1__AT1)))
+(let ((.def_119 (and .def_117 .def_118)))
+(let ((.def_114 (<= si_0__AT1 si_6__AT1)))
+(let ((.def_115 (not .def_114)))
+(let ((.def_116 (or sb_4__AT1 .def_115)))
+(let ((.def_120 (and .def_116 .def_119)))
+(let ((.def_111 (<= si_1__AT1 si_9__AT1)))
+(let ((.def_112 (not .def_111)))
+(let ((.def_113 (or sb_5__AT1 .def_112)))
+(let ((.def_121 (and .def_113 .def_120)))
+(let ((.def_122 (and sb_6__AT0 .def_121)))
+(let ((.def_123 (= sb_7__AT1 .def_122)))
+(let ((.def_170 (and .def_123 .def_169)))
+(let ((.def_110 (= si_13__AT1 si_14__AT1)))
+(let ((.def_171 (and .def_110 .def_170)))
+(let ((.def_100 (not sb_1__AT1)))
+(let ((.def_101 (or sb_2__AT1 .def_100)))
+(let ((.def_102 (= sb_0__AT1 .def_101)))
+(let ((.def_99 (= si_0__AT1 si_2__AT1)))
+(let ((.def_103 (and .def_99 .def_102)))
+(let ((.def_98 (= si_1__AT1 si_3__AT1)))
+(let ((.def_104 (and .def_98 .def_103)))
+(let ((.def_97 (= sb_1__AT1 sb_6__AT1)))
+(let ((.def_105 (and .def_97 .def_104)))
+(let ((.def_96 (= si_6__AT1 si_8__AT1)))
+(let ((.def_106 (and .def_96 .def_105)))
+(let ((.def_95 (= si_9__AT1 si_11__AT1)))
+(let ((.def_107 (and .def_95 .def_106)))
+(let ((.def_94 (= sb_6__AT1 sb_7__AT1)))
+(let ((.def_108 (and .def_94 .def_107)))
+(let ((.def_93 (= si_12__AT1 si_14__AT1)))
+(let ((.def_109 (and .def_93 .def_108)))
+(let ((.def_172 (and .def_109 .def_171)))
+(let ((.def_173 (and sb_0__AT0 .def_172)))
+.def_173
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+; (push 1)
+; (assert (let ((.def_174 (not sb_0__AT1)))
+; .def_174
+; ))
+; (check-sat)
+; (pop 1)
+
+(declare-fun sb_0__AT2 () Bool)
+(declare-fun si_0__AT2 () Int)
+(declare-fun si_1__AT2 () Int)
+(declare-fun sb_1__AT2 () Bool)
+(declare-fun si_2__AT2 () Int)
+(declare-fun si_3__AT2 () Int)
+(declare-fun sb_2__AT2 () Bool)
+(declare-fun si_4__AT2 () Int)
+(declare-fun si_5__AT2 () Int)
+(declare-fun sb_3__AT2 () Bool)
+(declare-fun sb_4__AT2 () Bool)
+(declare-fun sb_5__AT2 () Bool)
+(declare-fun si_6__AT2 () Int)
+(declare-fun si_7__AT2 () Int)
+(declare-fun si_8__AT2 () Int)
+(declare-fun si_9__AT2 () Int)
+(declare-fun si_10__AT2 () Int)
+(declare-fun si_11__AT2 () Int)
+(declare-fun sb_6__AT2 () Bool)
+(declare-fun sb_7__AT2 () Bool)
+(declare-fun si_12__AT2 () Int)
+(declare-fun si_13__AT2 () Int)
+(declare-fun si_14__AT2 () Int)
+(assert (let ((.def_267 (= si_0__AT1 si_2__AT2)))
+(let ((.def_266 (= si_1__AT1 si_3__AT2)))
+(let ((.def_268 (and .def_266 .def_267)))
+(let ((.def_259 (* (- 1) si_12__AT2)))
+(let ((.def_260 (+ si_1__AT2 .def_259)))
+(let ((.def_261 (+ si_0__AT2 .def_260)))
+(let ((.def_262 (<= .def_261 0)))
+(let ((.def_263 (not .def_262)))
+(let ((.def_264 (or sb_5__AT2 .def_263)))
+(let ((.def_265 (= sb_2__AT2 .def_264)))
+(let ((.def_269 (and .def_265 .def_268)))
+(let ((.def_251 (* (- 1) si_7__AT2)))
+(let ((.def_252 (+ si_6__AT1 .def_251)))
+(let ((.def_253 (= .def_252 (- 1))))
+(let ((.def_246 (not sb_3__AT1)))
+(let ((.def_254 (or .def_246 .def_253)))
+(let ((.def_248 (= si_7__AT2 0)))
+(let ((.def_249 (or sb_3__AT1 .def_248)))
+(let ((.def_255 (and .def_249 .def_254)))
+(let ((.def_243 (* (- 1) si_13__AT2)))
+(let ((.def_244 (+ si_12__AT1 .def_243)))
+(let ((.def_245 (= .def_244 (- 1))))
+(let ((.def_247 (or .def_245 .def_246)))
+(let ((.def_256 (and .def_247 .def_255)))
+(let ((.def_240 (= si_13__AT2 0)))
+(let ((.def_241 (or sb_3__AT1 .def_240)))
+(let ((.def_257 (and .def_241 .def_256)))
+(let ((.def_270 (and .def_257 .def_269)))
+(let ((.def_237 (not sb_4__AT1)))
+(let ((.def_234 (* (- 1) si_10__AT2)))
+(let ((.def_235 (+ si_9__AT1 .def_234)))
+(let ((.def_236 (= .def_235 (- 1))))
+(let ((.def_238 (or .def_236 .def_237)))
+(let ((.def_231 (= si_10__AT2 0)))
+(let ((.def_232 (or sb_4__AT1 .def_231)))
+(let ((.def_239 (and .def_232 .def_238)))
+(let ((.def_271 (and .def_239 .def_270)))
+(let ((.def_230 (= si_7__AT2 si_8__AT2)))
+(let ((.def_272 (and .def_230 .def_271)))
+(let ((.def_229 (= si_10__AT2 si_11__AT2)))
+(let ((.def_273 (and .def_229 .def_272)))
+(let ((.def_223 (<= 1 si_0__AT2)))
+(let ((.def_222 (<= 1 si_1__AT2)))
+(let ((.def_224 (and .def_222 .def_223)))
+(let ((.def_219 (<= si_0__AT2 si_6__AT2)))
+(let ((.def_220 (not .def_219)))
+(let ((.def_221 (or sb_4__AT2 .def_220)))
+(let ((.def_225 (and .def_221 .def_224)))
+(let ((.def_216 (<= si_1__AT2 si_9__AT2)))
+(let ((.def_217 (not .def_216)))
+(let ((.def_218 (or sb_5__AT2 .def_217)))
+(let ((.def_226 (and .def_218 .def_225)))
+(let ((.def_227 (and sb_6__AT1 .def_226)))
+(let ((.def_228 (= sb_7__AT2 .def_227)))
+(let ((.def_274 (and .def_228 .def_273)))
+(let ((.def_215 (= si_13__AT2 si_14__AT2)))
+(let ((.def_275 (and .def_215 .def_274)))
+(let ((.def_205 (not sb_1__AT2)))
+(let ((.def_206 (or sb_2__AT2 .def_205)))
+(let ((.def_207 (= sb_0__AT2 .def_206)))
+(let ((.def_204 (= si_0__AT2 si_2__AT2)))
+(let ((.def_208 (and .def_204 .def_207)))
+(let ((.def_203 (= si_1__AT2 si_3__AT2)))
+(let ((.def_209 (and .def_203 .def_208)))
+(let ((.def_202 (= sb_1__AT2 sb_6__AT2)))
+(let ((.def_210 (and .def_202 .def_209)))
+(let ((.def_201 (= si_6__AT2 si_8__AT2)))
+(let ((.def_211 (and .def_201 .def_210)))
+(let ((.def_200 (= si_9__AT2 si_11__AT2)))
+(let ((.def_212 (and .def_200 .def_211)))
+(let ((.def_199 (= sb_6__AT2 sb_7__AT2)))
+(let ((.def_213 (and .def_199 .def_212)))
+(let ((.def_198 (= si_12__AT2 si_14__AT2)))
+(let ((.def_214 (and .def_198 .def_213)))
+(let ((.def_276 (and .def_214 .def_275)))
+(let ((.def_277 (and sb_0__AT1 .def_276)))
+.def_277
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+(push 1)
+(assert (not sb_0__AT2))
+(check-sat)
+(pop 1)
+
diff --git a/test/regress/regress0/simplification_bug4.smt2.expect b/test/regress/regress0/simplification_bug4.smt2.expect
new file mode 100644
index 000000000..ef44f9b74
--- /dev/null
+++ b/test/regress/regress0/simplification_bug4.smt2.expect
@@ -0,0 +1,3 @@
+% COMMAND-LINE: --incremental
+% EXPECT: unsat
+% EXIT: 20
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 6c06175d2..75d81b938 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -102,12 +102,12 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
-  elif grep -q '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
-    expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes`
-    expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
-    expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
-    expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
-    command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
+  elif grep -q '^\(%\|;\) \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
+    expected_proof=`grep -q '^[%;] PROOF' "$benchmark" && echo yes`
+    expected_output=`grep '^[%;] EXPECT: ' "$benchmark" | sed 's,^[%;] EXPECT: ,,'`
+    expected_error=`grep '^[%;] EXPECT-ERROR: ' "$benchmark" | sed 's,^[%;] EXPECT-ERROR: ,,'`
+    expected_exit_status=`grep -m 1 '^[%;] EXIT: ' "$benchmark" | perl -pe 's,^[%;] EXIT: ,,;s,\r,,'`
+    command_line=`grep '^[%;] COMMAND-LINE: ' "$benchmark" | sed 's,^[%;] COMMAND-LINE: ,,'`
     # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
     # this frustrates our auto-language-detection
     gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 99e8b087c..e9cba5f9c 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -100,7 +100,11 @@ public:
     return SatValUnknown;
   }
 
-};
+  bool properExplanation(SatLiteral lit, SatLiteral expl) const {
+    return true;
+  }
+
+};/* class FakeSatSolver */
 
 class CnfStreamBlack : public CxxTest::TestSuite {
   /** The SAT solver proxy */