diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 86f30ed73..4e457d270 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -489,7 +489,6 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
                   tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n";
               });
         subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t);
-        SASSERT(is_well_sorted(m_manager, norm_t));
     }
     else {
         norm_t = t;
diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index 4d8849178..8f46139f7 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/src/ast/normal_forms/nnf.cpp
@@ -102,7 +102,6 @@ class skolemizer {
             }
         }
         s(body, substitution.size(), substitution.c_ptr(), r);
-        SASSERT(is_well_sorted(m(), r));
         p = 0;
         if (m().proofs_enabled()) {
             if (q->is_forall())