diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp
index e59a079e7..9c345851a 100644
--- a/src/ast/rewriter/quant_hoist.cpp
+++ b/src/ast/rewriter/quant_hoist.cpp
@@ -41,9 +41,9 @@ public:
         m_rewriter(m)
     {}
     
-    void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) {
+    void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) {
         quantifier_type qt = Q_none_pos;
-        pull_quantifier(fml, qt, vars, result);
+        pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
@@ -51,36 +51,38 @@ public:
         is_fa = (Q_forall_pos == qt);
     }
     
-    void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) {
+    void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
         quantifier_type qt = Q_exists_pos;
-        pull_quantifier(fml, qt, vars, result);
+        pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
     }
 
-    void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) {
+    void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) {
         quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos;
         expr_ref result(m);
-        pull_quantifier(fml, qt, vars, result);
+        pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
         fml = result;
     }
     
-    void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result) {
+    void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result, bool use_fresh) {
         unsigned nd = q->get_num_decls();
         for (unsigned i = 0; i < nd; ++i) {
             sort* s = q->get_decl_sort(i);
-            app* a = m.mk_fresh_const(q->get_decl_name(i).str().c_str(), s);
+            symbol const& sym = q->get_decl_name (i);
+            app* a = use_fresh ? m.mk_fresh_const(sym.str ().c_str (), s)
+                               : m.mk_const (sym, s);
             vars.push_back(a);
         }
         expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd);
         instantiate(m, q, exprs, result);
     }
 
-    unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
+    unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh, bool rewrite_ok) {
         unsigned index = var_counter().get_next_var(fml);
         while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
             quantifier* q = to_quantifier(fml);
@@ -97,7 +99,7 @@ public:
             return index;
         }
         app_ref_vector vars(m);
-        pull_quantifier(is_forall, fml, vars);
+        pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok);
         if (vars.empty()) {
             return index;
         }
@@ -192,7 +194,7 @@ private:
     }
     
     
-    void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) {
+    void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
         
         if (!has_quantifiers(fml)) {
             result = fml;
@@ -209,38 +211,48 @@ private:
             if (m.is_and(fml)) {
                 num_args = a->get_num_args();
                 for (unsigned i = 0; i < num_args; ++i) {
-                    pull_quantifier(a->get_arg(i), qt, vars, tmp);
+                    pull_quantifier(a->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
                     args.push_back(tmp);
                 }
+                if (rewrite_ok) {
                 m_rewriter.mk_and(args.size(), args.c_ptr(), result);
+            }
+                else {
+                    result = m.mk_and (args.size (), args.c_ptr ());
+                }
             }
             else if (m.is_or(fml)) {
                 num_args = to_app(fml)->get_num_args();
                 for (unsigned i = 0; i < num_args; ++i) {
-                    pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp);
+                    pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
                     args.push_back(tmp);
                 }
+                if (rewrite_ok) {
                 m_rewriter.mk_or(args.size(), args.c_ptr(), result);
+            }
+                else {
+                    result = m.mk_or (args.size (), args.c_ptr ());
+                }
             }
             else if (m.is_not(fml)) {
-                pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
+                pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp, use_fresh, rewrite_ok);
                 negate(qt);
                 result = m.mk_not(tmp);
             }
             else if (m.is_implies(fml, t1, t2)) {
-                pull_quantifier(t1, negate(qt), vars, tmp);
+                pull_quantifier(t1, negate(qt), vars, tmp, use_fresh, rewrite_ok);
                 negate(qt);
-                pull_quantifier(t2, qt, vars, result);
+                pull_quantifier(t2, qt, vars, result, use_fresh, rewrite_ok);
                 result = m.mk_implies(tmp, result);
             }
             else if (m.is_ite(fml, t1, t2, t3)) {
                 expr_ref tt1(m), tt2(m), tt3(m), ntt1(m), nt1(m);
-                pull_quantifier(t2, qt, vars, tt2);
-                pull_quantifier(t3, qt, vars, tt3);
+                pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok);
+                pull_quantifier(t3, qt, vars, tt3, use_fresh, rewrite_ok);
                 if (has_quantifiers(t1)) {
-                    pull_quantifier(t1, qt, vars, tt1);
+                    pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
                     nt1 = m.mk_not(t1);
-                    pull_quantifier(nt1, qt, vars, ntt1);
+                    pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
                     result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3));
                 }
                 else {
@@ -249,12 +261,12 @@ private:
             }
             else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) {
                 expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m);
-                pull_quantifier(t1, qt, vars, tt1);
-                pull_quantifier(t2, qt, vars, tt2);
+                pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
+                pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok);
                 nt1 = m.mk_not(t1);
                 nt2 = m.mk_not(t2);
-                pull_quantifier(nt1, qt, vars, ntt1);
-                pull_quantifier(nt2, qt, vars, ntt2);
+                pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
+                pull_quantifier(nt2, qt, vars, ntt2, use_fresh, rewrite_ok);
                 result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1));
             }
             else {
@@ -271,8 +283,8 @@ private:
                 break;
             }
             set_quantifier_type(qt, q->is_forall());
-            extract_quantifier(q, vars, tmp);
-            pull_quantifier(tmp, qt, vars, result);
+            extract_quantifier(q, vars, tmp, use_fresh);
+            pull_quantifier(tmp, qt, vars, result, use_fresh, rewrite_ok);
             break;
         }
         case AST_VAR:
@@ -295,18 +307,18 @@ quantifier_hoister::~quantifier_hoister() {
     dealloc(m_impl);
 }
 
-void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) {
-    (*m_impl)(fml, vars, is_fa, result);
+void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) {
+    (*m_impl)(fml, vars, is_fa, result, use_fresh, rewrite_ok);
 }
 
-void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) {
-    m_impl->pull_exists(fml, vars, result);
+void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
+    m_impl->pull_exists(fml, vars, result, use_fresh, rewrite_ok);
 }
 
-void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) {
-    m_impl->pull_quantifier(is_forall, fml, vars);
+void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) {
+    m_impl->pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok);
 }
 
-unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
-    return m_impl->pull_quantifier(is_forall, fml, sorts, names);
+unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh, bool rewrite_ok) {
+    return m_impl->pull_quantifier(is_forall, fml, sorts, names, use_fresh, rewrite_ok);
 }
diff --git a/src/ast/rewriter/quant_hoist.h b/src/ast/rewriter/quant_hoist.h
index 90e6ec7ad..52a2fcda1 100644
--- a/src/ast/rewriter/quant_hoist.h
+++ b/src/ast/rewriter/quant_hoist.h
@@ -43,14 +43,14 @@ public:
        or, and, implies, ite (then and else branch only).
     */
 
-    void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result);
+    void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
 
     /**
        \brief Pull top-most existential quantifier up.
 
        The list of variables is empty if there are no top-level existential quantifier.
     */
-    void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result);
+    void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
 
 
     /**
@@ -58,7 +58,7 @@ public:
 
        The list of variables is empty if there are no top-level universal/existential quantifier.
     */
-    void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars);
+    void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh = true, bool rewrite_ok = true);
 
     /**
        \brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up.
@@ -66,7 +66,7 @@ public:
        Return index of maximal variable.
     */
 
-    unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names);
+    unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh = true, bool rewrite_ok = true);
 
 };