From cb6eb0fc96f318851595629ab08bd9a2d518f374 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 23 Feb 2020 09:48:45 -0800
Subject: [PATCH] fix #3078

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/reduce_invertible_tactic.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 22b4b3395..b664a9e26 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -220,6 +220,9 @@ private:
 
             if (m_bv.is_numeral(arg, r) && r != mdl)
                 return false;
+
+            if (i > 0 && (!is_app(arg) || to_app(arg)->get_num_args() > 0))
+                return false;
         }
 
         if (mc) {