From bef6f1a72942045f0ec59a3ab79cd11bd4eca9ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Mar 2021 13:51:58 -0800 Subject: [PATCH] fix build --- scripts/mk_project.py | 2 +- src/sat/smt/euf_relevancy.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 19f87d0b5..28413965a 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -74,8 +74,8 @@ def init_project_def(): add_lib('ddnf', ['muz', 'transforms', 'rel'], 'muz/ddnf') add_lib('bmc', ['muz', 'transforms', 'fd_solver'], 'muz/bmc') add_lib('fp', ['muz', 'clp', 'tab', 'rel', 'bmc', 'ddnf', 'spacer'], 'muz/fp') - add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz', 'qe'], 'tactic/smtlogics') + add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter', 'smtlogic_tactics'], 'tactic/ufbv') add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa') add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'fd_solver', 'qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt') diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp index 4af05dc97..51388fa80 100644 --- a/src/sat/smt/euf_relevancy.cpp +++ b/src/sat/smt/euf_relevancy.cpp @@ -83,7 +83,7 @@ namespace euf { if (!is_app(e)) continue; expr* c = nullptr, *th = nullptr, *el = nullptr; - if (m.is_ite(e, c, th, el)) { + if (m.is_ite(e, c, th, el) && get_enode(c)) { sat::literal lit = expr2literal(c); todo.push_back(c); switch (s().value(lit)) {