From 07413cc9287fc1c02528c598e11824dfc131d063 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Apr 2020 12:56:52 -0700
Subject: [PATCH] fix #3785

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/rewriter_def.h        | 30 +++++++++++---------------
 src/muz/base/dl_rule.cpp               |  1 +
 src/muz/transforms/dl_mk_bit_blast.cpp | 13 ++++++-----
 3 files changed, 21 insertions(+), 23 deletions(-)

diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 963a8ad94..ecead81de 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -38,17 +38,10 @@ void rewriter_tpl<Config>::process_var(var * v) {
     unsigned idx = v->get_idx();
     if (ProofGen) {
         result_pr_stack().push_back(nullptr); // implicit reflexivity
-
-        SASSERT(
-            true || // disabled for now
-            idx >= m_bindings.size() ||
-            !m_bindings[m_bindings.size() - idx - 1] ||
-            v == m_bindings[m_bindings.size() - idx - 1]);
     }
     unsigned index = 0;
     expr * r;
-    if (!ProofGen && idx < m_bindings.size() && 
-        (index = m_bindings.size() - idx - 1, r = m_bindings[index])) {
+    if (idx < m_bindings.size() && (index = m_bindings.size() - idx - 1, r = m_bindings[index])) {
         CTRACE("rewriter", v->get_sort() != m().get_sort(r),
                tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m());
                tout << "index " << index << " bindings " << m_bindings.size() << "\n";
@@ -60,24 +53,25 @@ void rewriter_tpl<Config>::process_var(var * v) {
             expr* c = get_cached(r, shift_amount);
             if (c) {
                 result_stack().push_back(c);
-                set_new_child_flag(v);
-                return;
             }
-            expr_ref tmp(m());
-            m_shifter(r, shift_amount, tmp);
-            result_stack().push_back(tmp);
-            TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n";
-                  display_bindings(tout););
-            cache_shifted_result(r, shift_amount, tmp);                    
+            else {
+                expr_ref tmp(m());
+                m_shifter(r, shift_amount, tmp);
+                result_stack().push_back(tmp);
+                TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n";
+                      display_bindings(tout););
+                cache_shifted_result(r, shift_amount, tmp);                    
+            }
         }
         else {
             result_stack().push_back(r);
             TRACE("rewriter", tout << idx << " " << mk_ismt2_pp(r, m()) << "\n";);
         }
         set_new_child_flag(v);
-        return;
     }
-    result_stack().push_back(v);
+    else {
+        result_stack().push_back(v);
+    }
 }
 
 template<typename Config>
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 6ca1cf7ab..40b7df07d 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -570,6 +570,7 @@ namespace datalog {
         default: fml = m.mk_implies(m.mk_and(body.size(), body.c_ptr()), fml); break;
         }
 
+        m_free_vars.reset();        
         m_free_vars(fml);
         if (m_free_vars.empty()) {
             return;
diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp
index 992b8f51b..f2f149971 100644
--- a/src/muz/transforms/dl_mk_bit_blast.cpp
+++ b/src/muz/transforms/dl_mk_bit_blast.cpp
@@ -240,7 +240,7 @@ namespace datalog {
             m_context.get_rule_manager().to_formula(*r2.get(), fml1);
             m_blaster(fml1, fml2, pr);
             m_rewriter(fml2, fml3);
-            TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml2, m) << " -> " << mk_pp(fml3, m) << "\n";);
+            TRACE("dl", tout << fml << "\n-> " << fml1 << "\n-> " << fml2 << "\n-> " << fml3 << "\n";);
             if (fml3 != fml) {
                 fml = fml3;
                 return true;
@@ -268,6 +268,8 @@ namespace datalog {
             if (!m_context.xform_bit_blast()) {
                 return nullptr;
             }
+            if (m.proofs_enabled())
+                return nullptr;
             rule_manager& rm = m_context.get_rule_manager();
             unsigned sz = source.get_num_rules();
             expr_ref fml(m);
@@ -277,7 +279,9 @@ namespace datalog {
             for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) {
                 rule * r = source.get_rule(i);
                 rm.to_formula(*r, fml);
+                TRACE("dl", tout << fml << "\n";);
                 if (blast(r, fml)) {
+                    TRACE("dl", tout << "blasted: " << fml << "\n";);
                     proof_ref pr(m);
                     if (r->get_proof()) {
                         scoped_proof _sc(m);
@@ -295,10 +299,9 @@ namespace datalog {
 
             // copy output predicates without any rule (bit-blasting not really needed)
             const func_decl_set& decls = source.get_output_predicates();
-            for (func_decl_set::iterator I = decls.begin(), E = decls.end(); I != E; ++I) {
-                if (!source.contains(*I))
-                    result->set_output_predicate(*I);
-            }
+            for (func_decl* p : decls)
+                if (!source.contains(p))
+                    result->set_output_predicate(p);            
 
             if (m_context.get_model_converter()) {
                 generic_model_converter* fmc = alloc(generic_model_converter, m, "dl_mk_bit_blast");