mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

bv_bounds: early exit in is_bound in case the expr is not boolean

Browse source 
~2% speedup
This commit is contained in:
Nuno Lopes 2016-02-25 09:32:10 +00:00
parent 4e7a867cd9
commit c1aa33339d
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -162,6 +162,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
map *m_bound; map *m_bound;
bool is_bound(expr *e, expr*& v, interval& b) { bool is_bound(expr *e, expr*& v, interval& b) {
if (!m.is_bool(e))
return false;
rational n; rational n;
expr *lhs, *rhs; expr *lhs, *rhs;
unsigned sz; unsigned sz;