From 6f65051f2c5d917bc76668e40a89fbb97e16bbb4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Apr 2020 17:11:34 -0700 Subject: [PATCH] silence some build warnings Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 1 - src/smt/theory_arith_inv.h | 2 ++ src/tactic/arith/eq2bv_tactic.cpp | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 8dc6d0615..00c994471 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -169,7 +169,6 @@ namespace sat { init_goodvars(); set_best_unsat(); - unsigned sz = m_units.size(); for (unsigned i = 0; !m_is_unsat && i < m_units.size(); ++i) { bool_var v = m_units[i]; propagate(literal(v, !cur_solution(v))); diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h index a46cc3e02..e569d221a 100644 --- a/src/smt/theory_arith_inv.h +++ b/src/smt/theory_arith_inv.h @@ -191,6 +191,8 @@ namespace smt { template bool theory_arith::satisfy_bounds() const { + if (get_manager().limit().get_cancel_flag()) + return true; int num = get_num_vars(); for (theory_var v = 0; v < num; v++) { CTRACE("bound_bug", below_lower(v) || above_upper(v), display_var(tout, v); display(tout);); diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index 3a302993e..d0dbbc90c 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -212,7 +212,7 @@ public: bool strict = true; rational v; bool has_val = - (m_bounds.has_upper(var, v, strict) && !strict) && v.is_unsigned() || + (m_bounds.has_upper(var, v, strict) && !strict && v.is_unsigned()) || (m_bounds.has_lower(var, v, strict) && !strict && v.is_unsigned()); if (has_val) {