From 41c648905eeb6d99e96754d1ba6bfa0ef66ec4c1 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@anu.edu.au>
Date: Fri, 28 Apr 2017 21:35:21 +1000
Subject: [PATCH] fix(library/tactic/smt/ematch.cpp) check if new_states is
 empty before pushing

---
 src/library/tactic/smt/ematch.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/library/tactic/smt/ematch.cpp b/src/library/tactic/smt/ematch.cpp
index 9f4a282f77..7371b7cc03 100644
--- a/src/library/tactic/smt/ematch.cpp
+++ b/src/library/tactic/smt/ematch.cpp
@@ -697,6 +697,10 @@ class ematch_fn {
                 new_states.emplace_back(new_state, std::max(m_gen, gen));
             }
         }
+        if (new_states.empty()) {
+            lean_trace(name({"debug", "smt", "ematch"}), tout() << "(no new states)\n";);
+            return false;
+        }
         push_states(new_states);
         return true;
     }