From 5f0ec936e41242040b132f67102799f0a041f37e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 5 Mar 2021 15:01:02 -0800
Subject: [PATCH] count final checks

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

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 4a2d9f40d..0430ead12 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -440,6 +440,7 @@ namespace euf {
     }
 
     sat::check_result solver::check() { 
+        ++m_stats.m_final_checks;
         TRACE("euf", s().display(tout););
         bool give_up = false;
         bool cont = false;
@@ -686,6 +687,7 @@ namespace euf {
         for (auto* e : m_solvers)
             e->collect_statistics(st);
         st.update("euf ackerman", m_stats.m_ackerman);
+        st.update("euf final check", m_stats.m_final_checks);
     }
 
     enode* solver::copy(solver& dst_ctx, enode* src_n) {
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 5e5525be9..c2c2e0777 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -66,6 +66,7 @@ namespace euf {
         // friend class sat::ba_solver;
         struct stats {
             unsigned m_ackerman;
+            unsigned m_final_checks;
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };