diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp
index 47e3e3ef4..b7a2b4011 100644
--- a/src/smt/smt_relevancy.cpp
+++ b/src/smt/smt_relevancy.cpp
@@ -212,8 +212,8 @@ namespace smt {
                 return;
             case l_undef:
                 SASSERT(eh);
-                push_trail(eh_trail(n, val));
                 set_watches(n, val, new (get_region()) relevancy_ehs(eh, get_watches(n, val)));
+                push_trail(eh_trail(n, val));
                 break;
             case l_true:
                 eh->operator()(*this, n, val);
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 88bd6b92e..f207fa969 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -69,6 +69,12 @@ static void throw_out_of_memory() {
 }
 
 static void throw_alloc_counts_exceeded() {
+    #pragma omp critical (z3_memory_manager) 
+    {
+        // reset the count to avoid re-throwing while
+        // the exception is being thrown.
+        g_memory_alloc_count = 0;
+    }
     throw exceeded_memory_allocations();
 }