From 858ce1158d6b8708408a954bb08dba70cf1702d2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 4 Mar 2015 18:30:06 +0000 Subject: [PATCH] Bugfix in model translation (ast_manager mismatch after par-or). Thanks to stackoverflow user user297886 for reporting this issue. http://stackoverflow.com/questions/28852722/segmentation-fault-while-using-par-or-tactic Signed-off-by: Christoph M. Wintersteiger --- src/model/func_interp.cpp | 4 ++-- src/model/model.cpp | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index ae4c657bd..9110014bf 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -276,8 +276,8 @@ expr * func_interp::get_interp() const { return r; } -func_interp * func_interp::translate(ast_translation & translator) const { - func_interp * new_fi = alloc(func_interp, m_manager, m_arity); +func_interp * func_interp::translate(ast_translation & translator) const { + func_interp * new_fi = alloc(func_interp, translator.to(), m_arity); ptr_vector::const_iterator it = m_entries.begin(); ptr_vector::const_iterator end = m_entries.end(); diff --git a/src/model/model.cpp b/src/model/model.cpp index a6b9695b4..73a39a8eb 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -74,6 +74,7 @@ void model::register_decl(func_decl * d, expr * v) { void model::register_decl(func_decl * d, func_interp * fi) { SASSERT(d->get_arity() > 0); + SASSERT(&fi->m() == &m_manager); decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0); if (entry->get_data().m_value == 0) { // new entry