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