From d2bd92eab97bbc9528349b137d58f991f4805265 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 17 May 2021 10:42:34 -0700
Subject: [PATCH] fix #5271

---
 src/smt/smt_model_checker.cpp |  9 ++++++++-
 src/smt/smt_parallel.cpp      | 23 +++++++++++++++++------
 2 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index e0214972b..4598a9a3f 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -319,7 +319,14 @@ namespace smt {
     struct scoped_ctx_push {
         context* c;
         scoped_ctx_push(context* c): c(c) { c->push(); }
-        ~scoped_ctx_push() { c->pop(1); }
+        ~scoped_ctx_push() { 
+            try {
+                c->pop(1);
+            }
+            catch (...) {
+                ;
+            }
+        }
     };
 
     /**
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index e82b3f56e..744d5ce2b 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -193,14 +193,25 @@ namespace smt {
 
             }
             catch (z3_error & err) {
-                error_code = err.error_code();
-                ex_kind = ERROR_EX;                
-                done = true;
+                if (finished_id == UINT_MAX) {
+                    error_code = err.error_code();
+                    ex_kind = ERROR_EX;
+                    done = true;
+                }
             }
             catch (z3_exception & ex) {
-                ex_msg = ex.msg();
-                ex_kind = DEFAULT_EX;    
-                done = true;
+                if (finished_id == UINT_MAX) {
+                    ex_msg = ex.msg();
+                    ex_kind = DEFAULT_EX;
+                    done = true;
+                }
+            }
+            catch (...) {
+                if (finished_id == UINT_MAX) {
+                    ex_msg = "unknown exception";
+                    ex_kind = ERROR_EX;
+                    done = true;
+                }
             }
         };