From 1a396b0bd2eebe4f3ad7826cfec1fd8cbb7574cf Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 25 Nov 2014 18:13:24 +0000 Subject: [PATCH] [BV size reduction] fix bug in detection of signed upperbound Signed-off-by: Nuno Lopes --- src/tactic/bv/bv_size_reduction_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 5e32bf6c4..707a9284b 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -151,7 +151,7 @@ struct bv_size_reduction_tactic::imp { // bound is infeasible. } else { - update_signed_upper(to_app(lhs), val); + update_signed_upper(to_app(rhs), val); } } else update_signed_lower(to_app(rhs), val);