From e8141aaa84bb47a927282ce0318686fd12c7b2f9 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 12 Aug 2016 19:52:59 +0100
Subject: [PATCH] debug fixes

---
 src/ast/macros/macro_util.cpp   | 7 ++++---
 src/ast/rewriter/rewriter_def.h | 2 +-
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index ce8834cc7..bc2feafed 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -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);
     }
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 9c200a3e2..cd6a63acc 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -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()) {