From 16db8bf49e5dfd1ecb65431a97972ed471b80b06 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 11 Nov 2020 17:34:43 -0800
Subject: [PATCH] add model validation

---
 src/sat/smt/euf_model.cpp | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 1adb14d05..f845eb6e9 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -34,6 +34,7 @@ namespace euf {
         values2model(deps, mdl);
         for (auto* mb : m_solvers)
             mb->finalize_model(*mdl);
+        // validate_model(*mdl);
     }
 
     bool solver::include_func_interp(func_decl* f) {
@@ -196,5 +197,19 @@ namespace euf {
         return m_values2root;
     }
 
+    void solver::validate_model(model& mdl) {
+        for (enode* n : m_egraph.nodes()) {
+            expr* e = n->get_expr();
+            if (!m.is_bool(e))
+                continue;
+            unsigned id = n->get_root_id();
+            bool tt = m.is_true(m_values.get(id));
+            if (mdl.is_true(e) != tt) {
+                IF_VERBOSE(0, verbose_stream() << "Failed to evaluate " << id << " " << mk_bounded_pp(e, m) << "\n");
+            }
+        }
+        
+    }
+
 
 }