diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 4f6f4c3d7..aee136284 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;
-        } else {
-            base = e;
+            return true;
         }
-        return true;
+        base = e;
+        return !is_var(e);
     }
 
     static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) {