From 71ff987f6b2cc46756525ea636aebe05a23f9f9b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 5 Jun 2021 16:11:11 -0700
Subject: [PATCH] #5324

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

diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 886d37a58..85cf24021 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -248,10 +248,13 @@ namespace euf {
     }
 
     void solver::validate_model(model& mdl) {
+        bool first = true;
         for (enode* n : m_egraph.nodes()) {
             expr* e = n->get_expr();
             if (!m.is_bool(e))
                 continue;
+            if (has_quantifiers(e))
+                continue;
             if (!is_relevant(n))
                 continue;
             bool tt = l_true == s().value(n->bool_var());
@@ -263,6 +266,11 @@ namespace euf {
                        verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
                        for (auto* arg : euf::enode_args(n))
                            verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n";);
+            CTRACE("euf", first, 
+                   tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
+                   s().display(tout);
+                   tout << mdl << "\n";);
+            first = false;
         }
         
     }