revert fix for #2865

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Jan 22, 2020 · 0ab107d · 0ab107d
1 parent ad965ac
commit 0ab107d
Showing 1 changed file with 0 additions and 6 deletions.
diff --git 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) {