From 55f62fcaed255e47f7557e4f5dd6ecd04abd8e88 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Jan 2020 16:16:44 -0600 Subject: [PATCH] fix #2865 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_relevancy.h | 1 + src/smt/theory_fpa.cpp | 7 ++++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h index edaa237b8..25e9bb1ce 100644 --- a/src/smt/smt_relevancy.h +++ b/src/smt/smt_relevancy.h @@ -95,6 +95,7 @@ namespace smt { context & get_context() { return m_context; } + /** \brief Install an event handler that is invoked whenever n is marked as relevant. */ diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index bbb17750c..abad855c5 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -741,12 +741,13 @@ namespace smt { app* theory_fpa::get_ite_value(expr* e) { ast_manager & m = get_manager(); + context& ctx = get_context(); expr* e1, *e2, *e3; - while (m.is_ite(e, e1, e2, e3)) { - if (get_root(e2) == get_root(e)) { + while (m.is_ite(e, e1, e2, e3) && ctx.e_internalized(e)) { + if (ctx.get_enode(e2)->get_root() == ctx.get_enode(e)->get_root()) { e = e2; } - else if (get_root(e3) == get_root(e)) { + else if (ctx.get_enode(e3)->get_root() == ctx.get_enode(e)->get_root()) { e = e3; } else {