mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 12:48:53 +00:00
Code Activity

revert fix for #2865

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-22 15:06:20 -06:00
parent ad965ac896
commit 0ab107dcb5
1 changed files with 0 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_fpa.cpp
View file

@ -727,12 +727,6 @@ namespace smt {
context & ctx = get_context(); context & ctx = get_context();
m_factory = alloc(fpa_value_factory, m, get_family_id()); m_factory = alloc(fpa_value_factory, m, get_family_id());
mg.register_factory(m_factory); 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) { enode* theory_fpa::ensure_enode(expr* e) {