From bc8508f3df320508618ae3f18edd164cf1cf6464 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Mar 2014 17:59:49 -0700 Subject: [PATCH] patch bounds normalization bug found by dvitek Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/bv_size_reduction_tactic.cpp | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index c7d94f8f3..be84227c6 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -109,18 +109,6 @@ struct bv_size_reduction_tactic::imp { } } - void ensure_signed(app* lhs, numeral& n) { - - } - - bool at_upper(app* lhs, numeral const& n) { - return false; - } - - bool at_lower(app* lhs, numeral const& n) { - return false; - } - void collect_bounds(goal const & g) { unsigned sz = g.size(); numeral val;