From 76427cd2815f4648921209c7708f566ca05ba7ae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Jul 2021 11:33:47 -0700
Subject: [PATCH] #5427

---
 src/sat/tactic/goal2sat.cpp   | 4 ++++
 src/sat/tactic/goal2sat.h     | 2 ++
 src/sat/tactic/sat_tactic.cpp | 5 ++++-
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index b1332cdb2..72b825a09 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -999,6 +999,10 @@ bool goal2sat::has_interpreted_funs() const {
     return m_imp && !m_imp->interpreted_funs().empty(); 
 }
 
+bool goal2sat::has_euf() const {
+    return m_imp && m_imp->m_euf;
+}
+
 void goal2sat::update_model(model_ref& mdl) {
     if (m_imp) 
         m_imp->update_model(mdl);
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index 940777447..bc6b8dcb1 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -66,6 +66,8 @@ public:
 
     bool has_interpreted_funs() const;
 
+    bool has_euf() const;
+
     sat::sat_internalizer& si(ast_manager& m, params_ref const& p, sat::solver_core& t, atom2bool_var& a2b, dep2asm_map& dep2asm, bool default_external = false);
 
     void update_model(model_ref& mdl);
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 4d7b23166..c8c009bbf 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -113,8 +113,11 @@ class sat_tactic : public tactic {
                             break;
                         }
                     }
+
+                    bool euf = m_goal2sat.has_euf();
+		    
                     for (auto* f : fmls_to_validate) 
-                        if (md->is_false(f)) 
+                        if (!euf && md->is_false(f)) 
                             IF_VERBOSE(0, verbose_stream() << "failed to validate: " << mk_pp(f, m) << "\n";);
                     
                     m_goal2sat.update_model(md);