From 0ab107dcb534657d096c375075e0a756f729e3c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Jan 2020 15:06:20 -0600 Subject: [PATCH] revert fix for #2865 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_fpa.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index aafd1e00b3e..bbb17750cd8 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -727,12 +727,6 @@ namespace smt { context & ctx = get_context(); m_factory = alloc(fpa_value_factory, m, get_family_id()); mg.register_factory(m_factory); - - for (enode* n : ctx.enodes()) { - theory_var v = n->get_th_var(get_family_id()); - if (v != -1 && is_uninterp_const(n->get_owner())) - ctx.mark_as_relevant(n->get_owner()); - } } enode* theory_fpa::ensure_enode(expr* e) {