From fec94d1552fa7791618ee91a11b7a081be5e012e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Dec 2019 12:48:19 -0800 Subject: [PATCH] fix #2805 Signed-off-by: Nikolaj Bjorner --- src/tactic/fd_solver/bounded_int2bv_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp index 33a649194..4e7809530 100644 --- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp +++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp @@ -82,6 +82,7 @@ public: for (func_decl* f : m_bv_fns) result->m_bv_fns.push_back(tr(f)); for (func_decl* f : m_int_fns) result->m_int_fns.push_back(tr(f)); for (bound_manager* b : m_bounds) result->m_bounds.push_back(b->translate(dst_m)); + result->m_flushed = true; model_converter_ref mc = external_model_converter(); if (mc) { ast_translation tr(m, dst_m);