From 3a532c08a680beb1e5c8ba48a489cb87817a9d70 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 6 Apr 2016 19:24:08 +0100 Subject: [PATCH] Bugfix for func_interp else-case compression --- src/model/func_interp.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 7103c495d..5c53e64ba 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -141,8 +141,10 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector & args) { } void func_interp::set_else(expr * e) { + if (e == m_else) + return; + reset_interp_cache(); - m_manager.dec_ref(m_else); ptr_vector args; while (e && is_fi_entry_expr(e, args)) { @@ -152,6 +154,7 @@ void func_interp::set_else(expr * e) { } m_manager.inc_ref(e); + m_manager.dec_ref(m_else); m_else = e; }