diff --git a/src/muz/rel/dl_mk_partial_equiv.h b/src/muz/rel/dl_mk_partial_equiv.h
index f982952f1..be871f53e 100644
--- a/src/muz/rel/dl_mk_partial_equiv.h
+++ b/src/muz/rel/dl_mk_partial_equiv.h
@@ -30,7 +30,7 @@ namespace datalog {
         ast_manager & m;
         context &     m_context;
     public:
-        mk_partial_equivalence_transformer(context & ctx, unsigned priority=45000)
+        mk_partial_equivalence_transformer(context & ctx, unsigned priority=30000)
             : plugin(priority),
             m(ctx.get_manager()),
             m_context(ctx) {}
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 68bc25c27..6d167dfec 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -307,8 +307,8 @@ namespace datalog {
         if (m_context.similarity_compressor()) {
             transf.register_plugin(alloc(mk_similarity_compressor, m_context)); 
         }
-        transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
         transf.register_plugin(alloc(mk_rule_inliner, m_context));
+        transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
         transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
         transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
 
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 150198bab..585944263 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -596,7 +596,7 @@ namespace qe {
                 p = m_pols.back();
                 if (!m_is_relevant(e)) {
                     pop();
-                    insert(e, p, p?e:m.mk_not(e));
+                    insert(e, p, p?e:mk_not(m, e));
                     continue;
                 }
                 if (!is_app(e)) {
@@ -634,7 +634,7 @@ namespace qe {
                 }
                 else {
                     pop();
-                    insert(e, p, p?e:m.mk_not(e));
+                    insert(e, p, p?e:mk_not(m, e));
                 }
 
             }
@@ -1208,7 +1208,7 @@ namespace qe {
                 }
                 bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), fml);
                 
-                fml = m.mk_not(m.mk_iff(q, fml));
+                fml = mk_not(m, m.mk_iff(q, fml));
                 ast_smt_pp pp(m);
                 out << "; eliminate " << mk_pp(m_var, m) << "\n";
                 out << "(push)\n";
@@ -1303,12 +1303,7 @@ namespace qe {
             }
         }
         TRACE("qe_verbose", tout << "No plugin for " << mk_ismt2_pp(e, m) << "\n";);
-        if (p || m.is_not(e, e)) {
-            result = e;
-        } 
-        else {
-            result = m.mk_not(e);
-        }
+        result = p?e:mk_not(m, e);
     }
 
     void i_solver_context::mk_atom_fn::operator()(expr* e, bool p, expr_ref& result) {
@@ -1436,7 +1431,7 @@ namespace qe {
                 m_fml = f;
                 f = m_subfml;                
                 m_solver.assert_expr(f);
-            }           
+            }
             m_root.init(f);                       
             TRACE("qe", 
                   for (unsigned i = 0; i < num_vars; ++i) tout << mk_ismt2_pp(vars[i], m) << "\n";
@@ -1591,7 +1586,7 @@ namespace qe {
             }
             m_literals.reset();
             while (node) {
-                m_literals.push_back(m.mk_not(node->assignment()));
+                m_literals.push_back(mk_not(m, node->assignment()));
                 node = node->parent();
             }    
             add_literal(l1);
@@ -1865,7 +1860,7 @@ namespace qe {
         //
         app* mk_eq_value(app* b, rational const& vl) {
             if (m.is_bool(b)) {
-                if (vl.is_zero()) return m.mk_not(b);
+                if (vl.is_zero()) return to_app(mk_not(m, b));
                 if (vl.is_one()) return b;
                 UNREACHABLE();
             }        
@@ -2604,12 +2599,12 @@ namespace qe {
             TRACE("qe", tout << "variables extracted" << mk_pp(result, m) << "\n";);
 
             if (old_q->is_forall()) {
-                result = m.mk_not(result);
+                result = mk_not(m, result);
             }
             m_ctx.solve(result, vars);
             if (old_q->is_forall()) {
                 expr* e = 0;
-                result = m.is_not(result, e)?e:m.mk_not(result);
+                result = m.is_not(result, e)?e:mk_not(m, result);
             }       
             var_shifter shift(m);
             shift(result, vars.size(), result);