From 5af1e4bdf436d1217654cc55538ea14432baaeb0 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 22 Nov 2012 15:03:11 +0000 Subject: [PATCH] remove redudant is_well_sorted checks after var_subst var_subst already checks for well sortedness of the resulting expression Signed-off-by: Nuno Lopes --- src/ast/macros/macro_util.cpp | 1 - src/ast/normal_forms/nnf.cpp | 1 - 2 files changed, 2 deletions(-) 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())