From 15916091d167012814931655f0df2f6e58a8d3c8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 28 May 2021 14:38:41 -0700
Subject: [PATCH] fix #5307

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/mam.cpp | 2 ++
 1 file changed, 2 insertions(+)

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);