diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 25fe5c43d..f8d99f398 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1661,6 +1661,8 @@ namespace {
 
                 if (m_incompatible.empty()) {
                     // sequence starting at head is fully compatible
+                    if (!curr)
+                        return;
                     SASSERT(curr != 0);
                     SASSERT(curr->m_opcode == CHOOSE);
                     choose * first_child = static_cast<choose *>(curr);