From d8905885ed1cc7694f03d66bdb2dd78daeee2b9b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 7 Jun 2021 10:59:10 -0700
Subject: [PATCH] #5324

---
 src/sat/smt/bv_delay_internalize.cpp | 4 ++++
 src/sat/smt/bv_internalize.cpp       | 2 +-
 src/sat/smt/bv_solver.h              | 1 +
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp
index 5c0061019..ca4841656 100644
--- a/src/sat/smt/bv_delay_internalize.cpp
+++ b/src/sat/smt/bv_delay_internalize.cpp
@@ -73,6 +73,8 @@ namespace bv {
         SASSERT(e->get_num_args() >= 2);
         expr_ref_vector args(m);
         euf::enode* n = expr2enode(e);
+        if (!reflect())
+            return false;
         auto r1 = eval_bv(n);
         auto r2 = eval_args(n, args);
         if (r1 == r2)
@@ -356,6 +358,8 @@ namespace bv {
             return internalize_mode::no_delay_i;
         if (!get_config().m_bv_delay)
             return internalize_mode::no_delay_i;
+        if (!reflect())
+            return internalize_mode::no_delay_i;
         internalize_mode mode;
         switch (to_app(e)->get_decl_kind()) {
         case OP_BMUL: 
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 8e6867dc7..deadc5a63 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -137,7 +137,7 @@ namespace bv {
             return true;
 
         SASSERT(!n || !n->is_attached_to(get_id()));
-        bool suppress_args = !get_config().m_bv_reflect && !m.is_considered_uninterpreted(a->get_decl());
+        bool suppress_args = !reflect() && !m.is_considered_uninterpreted(a->get_decl());
         if (!n)
             n = mk_enode(e, suppress_args);
 
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index daf21a132..3d15c2cf1 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -259,6 +259,7 @@ namespace bv {
         void assert_bv2int_axiom(app * n);
         void assert_int2bv_axiom(app* n);
         void assert_ackerman(theory_var v1, theory_var v2);
+        bool reflect() const { return get_config().m_bv_reflect; }
 
         // delay internalize
         enum class internalize_mode {