From 006caea5ba38749258ea2b12d713c0c01778661c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 18 Feb 2020 23:11:45 -0800
Subject: [PATCH] fix #3042

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index d66810e8a..f484dcf1f 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -130,7 +130,7 @@ namespace smt {
                 v = dst_ctx.mk_bool_var(dst_f);
             }
             else {
-                dst_ctx.internalize_formula(dst_f, false);
+                dst_ctx.internalize_formula(dst_f, true);
                 v = dst_ctx.get_bool_var(dst_f);
             }
             b2v.setx(lit.var(), v, null_bool_var);