From 2e176a0e02f164dbd27c0260b183f47eb15b045c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Sep 2021 08:27:46 -0700
Subject: [PATCH] count lazy bindings

---
 src/sat/smt/q_ematch.cpp | 2 ++
 src/sat/smt/q_ematch.h   | 1 +
 2 files changed, 3 insertions(+)

diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 0969995723d..cb5144a2b8d 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -240,6 +240,7 @@ namespace q {
             b->m_nodes[i] = _binding[i];        
         binding::push_to_front(c.m_bindings, b);
         ctx.push(remove_binding(ctx, c, b));
+        ++m_stats.m_num_delayed_bindings;
     }
 
     void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) {
@@ -612,6 +613,7 @@ namespace q {
         st.update("q redundant", m_stats.m_num_redundant);
         st.update("q units",     m_stats.m_num_propagations);
         st.update("q conflicts", m_stats.m_num_conflicts);
+        st.update("q delayed bindings", m_stats.m_num_delayed_bindings);
     }
 
     std::ostream& ematch::display(std::ostream& out) const {
diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
index e871a607721..41e8445721c 100644
--- a/src/sat/smt/q_ematch.h
+++ b/src/sat/smt/q_ematch.h
@@ -41,6 +41,7 @@ namespace q {
             unsigned m_num_propagations;
             unsigned m_num_conflicts;
             unsigned m_num_redundant;
+            unsigned m_num_delayed_bindings;
             
             stats() { reset(); }