diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index aee136284..cfb9a1eb8 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -96,10 +96,10 @@ struct reduce_args_tactic::imp {
         expr *lhs, *rhs;
         if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) {
             base = rhs;
-            return true;
+        } else {
+            base = e;
         }
-        base = e;
-        return !is_var(e);
+        return !is_var(base);
     }
 
     static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) {