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);