From 6d427d9dae4f374107297b5bf0dd0fa5651c0d1b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Dec 2020 12:46:24 -0800 Subject: [PATCH] fix #4839 --- src/smt/theory_lra.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b4c76fc6e..c3d348cf7 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3222,6 +3222,14 @@ public: init_variable_values(); m_factory = alloc(arith_factory, m); mg.register_factory(m_factory); + if (m_model_is_initialized) { + expr_ref val(m); + unsigned nv = th.get_num_vars(); + for (unsigned v = 0; v < nv; ++v) + if (get_value(get_enode(v), val)) + m_factory->register_value(val); + + } TRACE("arith", display(tout);); }