mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

debug fixes

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-08-12 19:52:59 +01:00
parent 244c641234
commit e8141aaa84
2 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -482,12 +482,13 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
}
if (changed) {
// REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution.
var_subst subst(m_manager);
var_subst subst(m_manager, true);
TRACE("macro_util_bug",
tout << "head: " << mk_pp(head, m_manager) << "\n";
tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitituion:\n";
tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n";
for (unsigned i = 0; i < var_mapping.size(); i++) {
tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n";
if (var_mapping[i] != 0)
tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n";
});
subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t);
}

2
src/ast/rewriter/rewriter_def.h
View file

@ -39,7 +39,7 @@ void rewriter_tpl<Config>::process_var(var * v) {
unsigned idx = v->get_idx();
if (idx < m_bindings.size()) {
unsigned index = m_bindings.size() - idx - 1;
expr * r = m_bindings[index];
var * r = (var*)(m_bindings[index]);
if (r != 0) {
SASSERT(v->get_sort() == m().get_sort(r));
if (!is_ground(r) && m_shifts[index] != m_bindings.size()) {