From aed4619066f24546ff8370fc86e9be1773a68c4b Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Thu, 17 Mar 2016 13:14:43 +0000
Subject: [PATCH] reduce-args: fixed unsoundness introduced in my previous
 commit skip an UF arg if it's quantified e.g. forall a . f(a, b) -> f(b) (but
 not f)

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