From d272acc3ac4169aaf0e1db89d674f1ae6e64faf9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 19 Nov 2023 12:48:33 -0800
Subject: [PATCH] fix crash when api_solver sets reset_tracked_assertions

---
 src/cmd_context/cmd_context.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 6f04799f6..019b7fd4f 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1678,6 +1678,8 @@ void cmd_context::restore_assertions(unsigned old_sz) {
         SASSERT(m_assertions.empty());
         return;
     }
+    if (m_assertions.empty())
+        return;
     if (old_sz == m_assertions.size())
         return;
     SASSERT(old_sz < m_assertions.size());
@@ -2296,6 +2298,8 @@ vector<std::pair<expr*,expr*>> cmd_context::tracked_assertions() {
 }
 
 void cmd_context::reset_tracked_assertions() {
+    for (expr* a : m_assertion_names)
+        m().dec_ref(a);
     m_assertion_names.reset();
     for (expr* a : m_assertions)
         m().dec_ref(a);