From f951372f032ffb182895fbed54b16a4b7c0dd45e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Mar 2016 13:54:42 -0700 Subject: [PATCH] fix regression in internalizing bit-vectors, reported by Mikolas Janota Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 355c52f1e..6d8b8c1d9 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -257,8 +257,10 @@ public: if (m_preprocess) { m_preprocess->reset(); } + if (!m_bb_rewriter) { + m_bb_rewriter = alloc(bit_blaster_rewriter, m, m_params); + } params_ref simp2_p = m_params; - m_bb_rewriter = alloc(bit_blaster_rewriter, m, m_params); simp2_p.set_bool("som", true); simp2_p.set_bool("pull_cheap_ite", true); simp2_p.set_bool("push_ite_bv", false);