From f946fc516c6be500b6b4cd9ac627f3951f3cb0b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Mar 2020 19:18:59 -0700 Subject: [PATCH] copy usorts as well Signed-off-by: Nikolaj Bjorner --- src/tactic/model_converter.cpp | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 127c7ef10..c50904ffb 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -131,14 +131,9 @@ public: m = m_model; return; } - for (unsigned i = 0; i < m_model->get_num_constants(); ++i) { - func_decl* f = m_model->get_constant(i); - m->register_decl(f, m_model->get_const_interp(f)); - } - for (unsigned i = 0; i < m_model->get_num_functions(); ++i) { - func_decl* f = m_model->get_function(i); - m->register_decl(f, m_model->get_func_interp(f)->copy()); - } + m->copy_const_interps(*m_model.get()); + m->copy_func_interps(*m_model.get()); + m->copy_usort_interps(*m_model.get()); } void operator()(labels_vec & r) override {