From facb42139856fb995fbb0586eac56db351f78483 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Thu, 17 Mar 2016 13:27:07 +0000
Subject: [PATCH] reduce-args: fix unsoundness 2: f(v + 2), where b is
 quantified

---
 src/tactic/core/reduce_args_tactic.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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) {