diff --git a/src/test/expr_context_simplifier.cpp b/src/test/expr_context_simplifier.cpp
index 1ff4944d8..bd512b426 100644
--- a/src/test/expr_context_simplifier.cpp
+++ b/src/test/expr_context_simplifier.cpp
@@ -3,6 +3,16 @@
 #include "ast_pp.h"
 #include "reg_decl_plugins.h"
 
+static void check_equiv(ast_manager& m, expr* e1, expr* e2) {
+    front_end_params fp;
+    smt::solver solver(m, fp);
+    expr_ref equiv(m);
+    equiv = m.mk_not(m.mk_eq(e1,e2));
+    solver.assert_expr(equiv);
+    lbool is_sat = solver.check();
+    SASSERT(is_sat == l_false);
+}
+
 static void simplify_formula(ast_manager& m, expr* e) {
     expr_ref result(m);
     expr_context_simplifier simp(m);
@@ -11,8 +21,10 @@ static void simplify_formula(ast_manager& m, expr* e) {
 
     TRACE("expr_context_simplifier",
           tout 
-          << mk_pp(e, m) << " |-> " 
+          << mk_pp(e, m) << "\n|->\n" 
           << mk_pp(result.get(), m) << "\n";);
+
+    check_equiv(m, e, result);
     
 }
 
@@ -27,8 +39,15 @@ void tst_expr_context_simplifier() {
     parser->parse_string(
         "(benchmark samples :logic QF_LIA                         \n"
         " :extrafuns ((x Int) (y Int) (z Int) (u Int))            \n"
+        " :extrapreds ((p) (q) (r)) \n"
         " :formula (and (<= 1 x) (or (<= 1 x) (<= x y)))          \n"
         " :formula (and (<= 2 (ite (<= z 1) (ite (<= z 1) x y) (* 2 x))) (<= x y)) \n"
+        " :formula (or (and (not p) q (or (not r) (and (or (not p) q) r)))\
+                       (and (not p) q (or (and p (not q) r) (and (or (not p) q) (not r)))) \
+                       (and (or (and p (not q)) (and p q))\
+                            (or (and p q r) (and (or (not p) (not q)) (not r))))\
+                       (and (not p) (not q) (or (and (not p) q r) (and (or p (not q)) (not r))))\
+                       (and (not p) (not q) (or (not r) (and (or p (not q)) r))))\n"
         ")"
         );
 
diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp
index 3e8e8b16f..e25e140a5 100644
--- a/src/test/quant_elim.cpp
+++ b/src/test/quant_elim.cpp
@@ -60,6 +60,7 @@ static void test_formula(lbool expected_outcome, char const* fml) {
     std::ostringstream buffer;
     buffer << "(benchmark presburger :status unknown :logic AUFLIA :extrapreds ((p1) (p2) (p3)) "
            << ":extrafuns ((a Int) (b Int))\n"
+           << ":extrapreds ((p) (q) (r))\n"
            << ":datatypes ((list (nil) (cons (hd Int) (tl list))))\n"
            << ":datatypes ((cell (cnil) (ccons (car cell) (cdr cell))))\n"
            << ":extrasorts (U)\n"
@@ -76,6 +77,17 @@ static void test_formula(lbool expected_outcome, char const* fml) {
 
 void tst_quant_elim() {
 
+    test_formula(l_undef, "(exists ((p1 Bool) (q1 Bool) (r1 Bool))\
+                                    (and (or (not p1) (not q1) r1)\
+                                         (or (and (not p) (not q) (not p1) q1)\
+                                             (and (not p) q p1 (not q1))\
+                                             (and p (not q) p1 q1)\
+                                             (and p q p1 q1))\
+                                         (or (and (not r) (not r1))\
+                                             (and (= p p1) (= q q1) r r1)\
+                                             (and (not (and (= p p1) (= q q1))) (not (= r r1))))))");
+
+
     test_formula(l_false,"(forall (x Int) (y Int) (or (= x 0) (< (* 5 y) (* 6 x)) (> (* 5 y) (* 6 x))))");
 
     test_formula(l_false, "(forall (a Int) (b Int) (exists (x Int) (and (< a (* 20 x)) (< (* 20 x) b))))");
@@ -99,6 +111,8 @@ void tst_quant_elim() {
     test_formula(l_undef, "(exists (a Bool) (b Bool) (or (and p1 a) (and p2 (not b))))");
 
 
+
+
     test_formula(l_false, 
                  "(forall (x Int) (q1 Int) (q2 Int) (r1 Int) (r2 Int) "
                  "  (implies "