From 1bc6c6a2a597880d72934be66930400b468d5b52 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Mar 2020 16:04:35 -0700 Subject: [PATCH] fix #3221 Signed-off-by: Nikolaj Bjorner --- src/tactic/model_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 021bbc886..41b9a08ea 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -137,7 +137,7 @@ public: } for (unsigned i = m_model->get_num_functions(); i-- > 0; ) { func_decl* f = m_model->get_function(i); - m->register_decl(f, m_model->get_func_interp(f)); + m->register_decl(f, m_model->get_func_interp(f)->copy()); } }