mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

remove redudant is_well_sorted checks after var_subst

Browse source 
var_subst already checks for well sortedness of the resulting expression

Signed-off-by: Nuno Lopes <nuno.lopes@ist.utl.pt>
This commit is contained in:
Nuno Lopes 2012-11-22 15:03:11 +00:00
parent 0ccae8e2e3
commit 5af1e4bdf4
2 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/macros/macro_util.cpp
View file

@ -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"; tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n";
}); });
subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t); subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t);
SASSERT(is_well_sorted(m_manager, norm_t));
} }
else { else {
norm_t = t; norm_t = t;

1
src/ast/normal_forms/nnf.cpp
View file

@ -102,7 +102,6 @@ class skolemizer {
} }
} }
s(body, substitution.size(), substitution.c_ptr(), r); s(body, substitution.size(), substitution.c_ptr(), r);
SASSERT(is_well_sorted(m(), r));
p = 0; p = 0;
if (m().proofs_enabled()) { if (m().proofs_enabled()) {
if (q->is_forall()) if (q->is_forall())