From 3764eb1959252238b24d198f846979fda231dced Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Sep 2021 00:24:34 -0700
Subject: [PATCH] #5532

ensure re-internalization for predicates that are replayed.
Theory internalization is currently not considered in depth.
---
 src/sat/smt/euf_model.cpp  | 17 ++++++++++++++---
 src/sat/smt/euf_solver.cpp | 15 +++++++++++----
 2 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index a297d79515e..6d183dec3af 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -266,14 +266,25 @@ namespace euf {
 
     void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
         out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
-        for (auto* arg : euf::enode_args(n)) {
-            expr_ref val = mdl(arg->get_expr());
+        euf::enode_vector nodes;
+        nodes.push_back(n);
+        for (unsigned i = 0; i < nodes.size(); ++i) {
+            euf::enode* r = nodes[i];
+            if (r->is_marked1())
+                continue;
+            r->mark1();
+            for (auto* arg : euf::enode_args(r))
+                nodes.push_back(arg);           
+            expr_ref val = mdl(r->get_expr());
             expr_ref sval(m);
             th_rewriter rw(m);
             rw(val, sval);
-            out << bpp(arg) << "\n" << sval << "\n";
+            out << bpp(r) << " := " << sval << " " << mdl(r->get_root()->get_expr()) << "\n";
         }
+        for (euf::enode* r : nodes)
+            r->unmark1();
         out << mdl << "\n";
+        s().display(out);
     }
 
     void solver::validate_model(model& mdl) {
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 54a47476b36..fe91914a7ee 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -454,6 +454,9 @@ namespace euf {
         bool give_up = false;
         bool cont = false;
 
+        if (unit_propagate())
+            return sat::check_result::CR_CONTINUE;
+
         if (!init_relevancy())
             give_up = true;
         
@@ -590,10 +593,14 @@ namespace euf {
                 lit = literal(replay.m[e], false);
             else 
                 lit = si.internalize(e, true);
-            VERIFY(lit.var() == v);          
-            if (is_app(e))
-                for (expr* arg : *to_app(e))
-                    e_internalize(arg);
+            VERIFY(lit.var() == v);     
+            if (!m_egraph.find(e) && (!m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e))) {
+                ptr_buffer<euf::enode> args;
+                if (is_app(e))
+                    for (expr* arg : *to_app(e))
+                        args.push_back(e_internalize(arg));
+                mk_enode(e, args.size(), args.data());
+            }
             attach_lit(lit, e);            
         }