From 648568489c064e3e8ac28ba3cf49dd309e5cb0cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Mar 2021 06:53:14 -0700 Subject: [PATCH] internalize only terms not atoms Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 15051bf05..40858e3f4 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -340,7 +340,7 @@ namespace smt { void context::ensure_internalized(expr* e) { if (!e_internalized(e)) internalize(e, false); - if (is_app(e)) + if (is_app(e) && !m.is_bool(e)) internalize_term(to_app(e)); }