From b3db9a1cd5a8eb80345e1ced9e1c1a11c95aad30 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Aug 2021 08:30:08 -0700 Subject: [PATCH] #5488 --- src/tactic/core/reduce_invertible_tactic.cpp | 2 ++ 1 file changed, 2 insertions(+) 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))