From e455897178b9bd64dcd01316df998b91c2948af9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Dec 2022 04:36:06 -0800
Subject: [PATCH] fix #6476

---
 src/tactic/ufbv/ufbv_rewriter.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp
index bfaf35980..a6a4e1957 100644
--- a/src/tactic/ufbv/ufbv_rewriter.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter.cpp
@@ -735,6 +735,8 @@ struct match_args_aux_proc {
                 m_subst.insert(n, 0, expr_offset(n, 1));
             }
         }
+        else
+            throw no_match();
     }
     void operator()(quantifier * n) { throw no_match(); }
     void operator()(app * n) {}