From 16ad33bf399d1b9aa1e333bbb89b560ffc868632 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jun 2016 18:15:51 -0700 Subject: [PATCH] add collection of statistics #652 Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/tactic/core/CMakeLists.txt | 1 + src/tactic/probe.cpp | 16 ++++++++-------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/contrib/cmake/src/tactic/core/CMakeLists.txt b/contrib/cmake/src/tactic/core/CMakeLists.txt index ed3a84edf..fcd26bd84 100644 --- a/contrib/cmake/src/tactic/core/CMakeLists.txt +++ b/contrib/cmake/src/tactic/core/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(core_tactics blast_term_ite_tactic.cpp cofactor_elim_term_ite.cpp cofactor_term_ite_tactic.cpp + collect_statistics_tactic.cpp ctx_simplify_tactic.cpp der_tactic.cpp distribute_forall_tactic.cpp diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index ecc27eccf..677438cdf 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -287,14 +287,14 @@ struct is_non_qfbv_predicate { if (fid == m.get_basic_family_id()) return; if (fid == u.get_family_id()) { - if (n->get_decl_kind() == OP_BSDIV0 || - n->get_decl_kind() == OP_BUDIV0 || - n->get_decl_kind() == OP_BSREM0 || - n->get_decl_kind() == OP_BUREM0 || - n->get_decl_kind() == OP_BSMOD0) - throw found(); - return; - } + if (n->get_decl_kind() == OP_BSDIV0 || + n->get_decl_kind() == OP_BUDIV0 || + n->get_decl_kind() == OP_BSREM0 || + n->get_decl_kind() == OP_BUREM0 || + n->get_decl_kind() == OP_BSMOD0) + throw found(); + return; + } if (is_uninterp_const(n)) return; throw found();