diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 57df65e83..a60f20aab 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -238,6 +238,8 @@ private:
             }
         }
         else {            
+            if (!is_uninterp_const(fst_arg))
+                return false;
             bool first = true;
             for (expr* arg : *a) {
                 if (!is_app(arg))