From 92065462b49c8bcbd060507cc0df0f93945c7114 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 4 Nov 2024 11:08:15 -0800
Subject: [PATCH] use std::exception as base class to z3_exception

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_config_params.cpp                  |  8 ++++----
 src/api/api_context.cpp                        |  4 ++--
 src/api/api_opt.cpp                            |  4 ++--
 src/api/api_parsers.cpp                        |  4 ++--
 src/api/z3_replayer.cpp                        |  2 +-
 src/ast/ast.cpp                                |  2 +-
 src/ast/sls/sat_ddfw.cpp                       |  2 +-
 src/cmd_context/basic_cmds.cpp                 |  2 +-
 src/cmd_context/cmd_context.cpp                |  8 ++++----
 src/cmd_context/eval_cmd.cpp                   |  2 +-
 src/cmd_context/simplify_cmd.cpp               |  2 +-
 src/cmd_context/tactic_cmds.cpp                |  6 +++---
 src/math/subpaving/tactic/subpaving_tactic.cpp |  2 +-
 src/model/model.cpp                            |  2 +-
 src/model/model_evaluator.cpp                  |  2 +-
 src/muz/fp/datalog_parser.cpp                  |  4 ++--
 src/muz/fp/dl_cmds.cpp                         |  4 ++--
 src/muz/fp/horn_tactic.cpp                     |  2 +-
 src/nlsat/tactic/nlsat_tactic.cpp              |  2 +-
 src/opt/maxsmt.cpp                             |  2 +-
 src/parsers/smt2/smt2parser.cpp                | 18 +++++++++---------
 src/sat/sat_solver.cpp                         |  2 +-
 src/sat/sat_solver/inc_sat_solver.cpp          | 10 +++++-----
 src/sat/sat_solver/sat_smt_solver.cpp          |  4 ++--
 src/sat/tactic/sat_tactic.cpp                  |  4 ++--
 src/shell/main.cpp                             |  2 +-
 src/shell/opt_frontend.cpp                     |  2 +-
 src/shell/z3_log_frontend.cpp                  |  2 +-
 src/smt/proto_model/proto_model.cpp            |  2 +-
 src/smt/smt_parallel.cpp                       |  2 +-
 src/smt/tactic/smt_tactic_core.cpp             |  2 +-
 src/smt/theory_bv.cpp                          |  2 +-
 src/solver/combined_solver.cpp                 |  2 +-
 src/solver/parallel_tactical.cpp               |  4 ++--
 src/solver/solver.cpp                          |  2 +-
 src/solver/tactic2solver.cpp                   |  9 ++++-----
 src/tactic/arith/factor_tactic.cpp             |  2 +-
 src/tactic/arith/fix_dl_var_tactic.cpp         |  2 +-
 src/tactic/arith/lia2pb_tactic.cpp             |  2 +-
 src/tactic/arith/normalize_bounds_tactic.cpp   |  2 +-
 src/tactic/arith/purify_arith_tactic.cpp       |  2 +-
 src/tactic/arith/recover_01_tactic.cpp         |  2 +-
 src/tactic/bv/bit_blaster_tactic.cpp           |  2 +-
 src/tactic/core/propagate_values_tactic.cpp    |  2 +-
 src/tactic/core/simplify_tactic.cpp            |  2 +-
 src/tactic/dependent_expr_state_tactic.h       |  2 +-
 src/tactic/fpa/fpa2bv_tactic.cpp               |  2 +-
 src/tactic/tactic.cpp                          |  4 ++--
 src/tactic/tactic_exception.h                  |  2 +-
 src/tactic/tactical.cpp                        | 10 +++++-----
 src/test/ex.cpp                                | 11 +++++------
 src/test/main.cpp                              |  2 +-
 src/test/mpff.cpp                              |  2 +-
 src/test/udoc_relation.cpp                     |  2 +-
 src/test/vector.cpp                            |  2 +-
 src/util/checked_int64.h                       |  4 ++--
 src/util/mpff.h                                |  6 +++---
 src/util/mpfx.h                                |  6 +++---
 src/util/z3_exception.cpp                      |  4 ++--
 src/util/z3_exception.h                        |  8 ++++----
 60 files changed, 109 insertions(+), 111 deletions(-)

diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
index d463b1fb7a6..193693874b4 100644
--- a/src/api/api_config_params.cpp
+++ b/src/api/api_config_params.cpp
@@ -36,7 +36,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            warning_msg("%s", ex.msg());
+            warning_msg("%s", ex.what());
         }
     }
 
@@ -59,7 +59,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            warning_msg("%s", ex.msg());
+            warning_msg("%s", ex.what());
             return false;
         }
     }
@@ -84,7 +84,7 @@ extern "C" {
         } catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            warning_msg("%s", ex.msg());
+            warning_msg("%s", ex.what());
             return nullptr;
         }
     }
@@ -106,7 +106,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            warning_msg("%s", ex.msg());
+            warning_msg("%s", ex.what());
         }
     }
 
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 2f1f5071221..6f7a424ea11 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -306,7 +306,7 @@ namespace api {
                 set_error_code(Z3_MEMOUT_FAIL, nullptr);
             break;
             case ERR_PARSER: 
-                set_error_code(Z3_PARSER_ERROR, ex.msg());
+                set_error_code(Z3_PARSER_ERROR, ex.what());
                 break;
             case ERR_INI_FILE: 
                 set_error_code(Z3_INVALID_ARG, nullptr);
@@ -320,7 +320,7 @@ namespace api {
             }
         }
         else {
-            set_error_code(Z3_EXCEPTION, ex.msg()); 
+            set_error_code(Z3_EXCEPTION, ex.what()); 
         }
     }
     
diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index a9a0b3230b5..e8566aa84ad 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -168,7 +168,7 @@ extern "C" {
                 }
                 r = l_undef;
                 if (!mk_c(c)->m().inc()) {
-                    to_optimize_ptr(o)->set_reason_unknown(ex.msg());
+                    to_optimize_ptr(o)->set_reason_unknown(ex.what());
                 }
                 else {
                     mk_c(c)->handle_exception(ex);
@@ -364,7 +364,7 @@ extern "C" {
             }        
         }
         catch (z3_exception& e) {
-            errstrm << e.msg();
+            errstrm << e.what();
             ctx = nullptr;
             SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
             return;
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index 94a955d4bf8..a43515da6ae 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -144,7 +144,7 @@ extern "C" {
         catch (z3_exception& e) {
             if (owned)
                 ctx = nullptr;
-            errstrm << e.msg();
+            errstrm << e.what();
             SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
             return of_ast_vector(v);
         }
@@ -257,7 +257,7 @@ extern "C" {
             }
         }
         catch (z3_exception& e) {
-            if (ous.str().empty()) ous << e.msg();
+            if (ous.str().empty()) ous << e.what();
             SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
             RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
         }
diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index 92f2c2d6a0c..eb6064a43cc 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -533,7 +533,7 @@ struct z3_replayer::imp {
                     throw;
                 }
                 catch (z3_exception & ex) {
-                    std::cout << "[z3 exception]: " << ex.msg() << std::endl;
+                    std::cout << "[z3 exception]: " << ex.what() << std::endl;
                 }
                 break;
             }
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index c4f87e5da98..d7ef4dc3e5a 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2080,7 +2080,7 @@ bool ast_manager::check_sorts(ast const * n) const {
         return true;
     }
     catch (ast_exception & ex) {
-        warning_msg("%s", ex.msg());
+        warning_msg("%s", ex.what());
         return false;
     }
 }
diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index 5473271ffcb..5129c2caff6 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -74,7 +74,7 @@ namespace sat {
             }
         }
         catch (z3_exception& ex) {
-            IF_VERBOSE(0, verbose_stream() << "Exception: " << ex.msg() << "\n");
+            IF_VERBOSE(0, verbose_stream() << "Exception: " << ex.what() << "\n");
             throw;
         }
         m_plugin->finish_search();
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index beb3aa0bb41..bc5990ef76b 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -439,7 +439,7 @@ class set_option_cmd : public set_get_option_cmd {
             ctx.global_params_updated();
         }
         catch (const gparams::exception & ex) {
-            throw cmd_exception(ex.msg());
+            throw cmd_exception(ex.what());
         }
     }
 
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 577cc95b624..1eed8a06738 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1605,7 +1605,7 @@ void cmd_context::push() {
         throw ex;
     }
     catch (z3_exception & ex) {
-        throw cmd_exception(ex.msg());
+        throw cmd_exception(ex.what());
     }
 }
 
@@ -1768,7 +1768,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
             throw ex;
         }
         catch (z3_exception & ex) {
-            throw cmd_exception(ex.msg());
+            throw cmd_exception(ex.what());
         }
         get_opt()->set_status(r);
     }
@@ -1793,7 +1793,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
                 m_solver->set_reason_unknown(eh);
             }
             else {
-                m_solver->set_reason_unknown(ex.msg());
+                m_solver->set_reason_unknown(ex.what());
             }
             r = l_undef;
         }
@@ -1832,7 +1832,7 @@ void cmd_context::get_consequences(expr_ref_vector const& assumptions, expr_ref_
         throw ex;
     }
     catch (z3_exception & ex) {
-        m_solver->set_reason_unknown(ex.msg());
+        m_solver->set_reason_unknown(ex.what());
         r = l_undef;
     }
     m_solver->set_status(r);
diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp
index 70a48da5f6b..93fa54ace7e 100644
--- a/src/cmd_context/eval_cmd.cpp
+++ b/src/cmd_context/eval_cmd.cpp
@@ -86,7 +86,7 @@ class eval_cmd : public parametric_cmd {
                 ev(m_target, r);
             }
             catch (model_evaluator_exception & ex) {
-                ctx.regular_stream() << "(error \"evaluator failed: " << ex.msg() << "\")" << std::endl;
+                ctx.regular_stream() << "(error \"evaluator failed: " << ex.what() << "\")" << std::endl;
                 return;
             }
         }
diff --git a/src/cmd_context/simplify_cmd.cpp b/src/cmd_context/simplify_cmd.cpp
index d5200374cf6..a989df0391b 100644
--- a/src/cmd_context/simplify_cmd.cpp
+++ b/src/cmd_context/simplify_cmd.cpp
@@ -89,7 +89,7 @@ class simplify_cmd : public parametric_cmd {
                 throw ex;
             }
             catch (z3_exception & ex) {
-                ctx.regular_stream() << "(error \"simplifier failed: " << ex.msg() << "\")" << std::endl;
+                ctx.regular_stream() << "(error \"simplifier failed: " << ex.what() << "\")" << std::endl;
                 failed = true;
                 r = m_target;
             }
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index b2b858b07ea..539e0915b30 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -227,8 +227,8 @@ class check_sat_using_tactic_cmd : public exec_given_tactic_cmd {
                 }
                 catch (z3_exception & ex) {
                     result->set_status(l_undef);
-                    result->m_unknown = ex.msg();
-                    ctx.regular_stream() << "(error \"tactic failed: " << ex.msg() << "\")" << std::endl;
+                    result->m_unknown = ex.what();
+                    ctx.regular_stream() << "(error \"tactic failed: " << ex.what() << "\")" << std::endl;
                 }
                 ctx.validate_check_sat_result(r);
             }
@@ -321,7 +321,7 @@ class apply_tactic_cmd : public exec_given_tactic_cmd {
                     exec(t, g, result_goals);
                 }
                 catch (tactic_exception & ex) {
-                    ctx.regular_stream() << "(error \"tactic failed: " << ex.msg() << "\")" << std::endl;
+                    ctx.regular_stream() << "(error \"tactic failed: " << ex.what() << "\")" << std::endl;
                     failed = true;
                 }
             }
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index 639528a7f47..f1b0e885486 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -252,7 +252,7 @@ class subpaving_tactic : public tactic {
         }
         catch (z3_exception & ex) {
             // convert all Z3 exceptions into tactic exceptions
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
     
diff --git a/src/model/model.cpp b/src/model/model.cpp
index ce2f3402e57..f8ef6897d82 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -95,7 +95,7 @@ bool model::eval_expr(expr * e, expr_ref & result, bool model_completion) {
     }
     catch (model_evaluator_exception & ex) {
         (void)ex;
-        TRACE("model_evaluator", tout << ex.msg() << "\n";);
+        TRACE("model_evaluator", tout << ex.what() << "\n";);
         return false;
     }
 }
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 6db52a98e61..069acc4d9b5 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -853,7 +853,7 @@ bool model_evaluator::eval(expr* t, expr_ref& r, bool model_completion) {
     }
     catch (model_evaluator_exception &ex) {
         (void)ex;
-        TRACE("model_evaluator", tout << ex.msg () << "\n";);
+        TRACE("model_evaluator", tout << ex.what () << "\n";);
         return false;
     }
 }
diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index c6df500d8b9..f736e5eb072 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -545,7 +545,7 @@ class dparser : public parser {
             result = tok == TK_EOS && m_error == false;
         }
         catch (z3_exception& ex) {
-            std::cerr << ex.msg() << std::endl;
+            std::cerr << ex.what() << std::endl;
             result = false;
         }
         return result;
@@ -1225,7 +1225,7 @@ class wpa_parser_impl : public wpa_parser, dparser {
             result = parse_directory_core(path);
         }
         catch (z3_exception& ex) {
-            std::cerr << ex.msg() << std::endl;
+            std::cerr << ex.what() << std::endl;
             return false;
         }
         return result;
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 508b79acea2..78aecfbed77 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -264,12 +264,12 @@ class dl_query_cmd : public parametric_cmd {
                 status = dlctx.rel_query(1, &m_target);
             }
             catch (z3_error & ex) {
-                ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl;
+                ctx.regular_stream() << "(error \"query failed: " << ex.what() << "\")" << std::endl;
                 print_statistics(ctx);
                 throw ex;
             }
             catch (z3_exception& ex) {
-                ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl;
+                ctx.regular_stream() << "(error \"query failed: " << ex.what() << "\")" << std::endl;
                 query_exn = true;
             }
         }
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 1a58bc92b92..c16523be075 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -255,7 +255,7 @@ class horn_tactic : public tactic {
                 is_reachable = m_ctx.query(q);
             }
             catch (default_exception& ex) {
-                IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";);
+                IF_VERBOSE(1, verbose_stream() << ex.what() << "\n";);
                 throw ex;
             }
             g->inc_depth();
diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp
index 11c80de2abb..aec39354cfe 100644
--- a/src/nlsat/tactic/nlsat_tactic.cpp
+++ b/src/nlsat/tactic/nlsat_tactic.cpp
@@ -249,7 +249,7 @@ class nlsat_tactic : public tactic {
         }
         catch (z3_exception & ex) {
             // convert all Z3 exceptions into tactic exceptions.
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
     
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index e684c64d6d0..721dae71168 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -214,7 +214,7 @@ namespace opt {
                 is_sat = (*m_msolver)();
             }
             catch (z3_exception& ex) {
-                IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n");
+                IF_VERBOSE(1, verbose_stream() << ex.what() << "\n");
                 is_sat = l_undef;
             }
             if (is_sat != l_false) {
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index afa36153861..70e324396b5 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -375,7 +375,7 @@ namespace smt2 {
                 }
                 catch (scanner_exception & ex) {
                     if (ex.has_pos())
-                        error(ex.line(), ex.pos(), ex.msg());
+                        error(ex.line(), ex.pos(), ex.what());
                     ++num_errors;
                 }
             }
@@ -3146,7 +3146,7 @@ namespace smt2 {
                 }
             }
             catch (z3_exception & ex) {
-                error(ex.msg());
+                error(ex.what());
             }
             return sexpr_ref(nullptr, sm());
         }
@@ -3162,7 +3162,7 @@ namespace smt2 {
                     return sort_ref(sort_stack().back(), m());
             }
             catch (z3_exception & ex) {
-                error(ex.msg());
+                error(ex.what());
             }
             return sort_ref(nullptr, m());
         }
@@ -3176,7 +3176,7 @@ namespace smt2 {
                 scan_core();
             }
             catch (scanner_exception & ex) {
-                error(ex.msg());
+                error(ex.what());
                 if (!sync_after_error())
                     return false;
                 found_errors++;
@@ -3202,7 +3202,7 @@ namespace smt2 {
                     // Can't invoke error(...) when out of memory.
                     // Reason: escaped() string builder needs memory
                     m_ctx.regular_stream() << "(error \"line " << m_scanner.get_line() << " column " << m_scanner.get_pos()
-                                           << ": " << ex.msg() << "\")" << std::endl;
+                                           << ": " << ex.what() << "\")" << std::endl;
                     exit(ex.error_code());
                 }
                 catch (const stop_parser_exception &) {
@@ -3211,15 +3211,15 @@ namespace smt2 {
                 }
                 catch (parser_exception & ex) {
                     if (ex.has_pos())
-                        error(ex.line(), ex.pos(), ex.msg());
+                        error(ex.line(), ex.pos(), ex.what());
                     else
-                        error(ex.msg());
+                        error(ex.what());
                 }
                 catch (ast_exception & ex) {
-                    error(ex.msg());
+                    error(ex.what());
                 }
                 catch (z3_exception & ex) {
-                    error(ex.msg());
+                    error(ex.what());
                 }
                 m_scanner.stop_caching();
                 if (m_curr_cmd)
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 69f3c0f377b..e6d35659850 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1564,7 +1564,7 @@ namespace sat {
                 ex_kind = ERROR_EX;                
             }
             catch (z3_exception & ex) {
-                ex_msg = ex.msg();
+                ex_msg = ex.what();
                 ex_kind = DEFAULT_EX;    
             }
         };
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 9b77b648276..ba972c61795 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -227,10 +227,10 @@ class inc_sat_solver : public solver {
             r = m_solver.check(m_asms.size(), m_asms.data());
         }
         catch (z3_exception& ex) {
-            IF_VERBOSE(1, verbose_stream() << "exception: " << ex.msg() << "\n";);
+            IF_VERBOSE(1, verbose_stream() << "exception: " << ex.what() << "\n";);
             if (m.inc()) {
                 reason_set = true;
-                set_reason_unknown(std::string("(sat.giveup ") + ex.msg() + ')');
+                set_reason_unknown(std::string("(sat.giveup ") + ex.what() + ')');
             }
             r = l_undef;            
         }
@@ -779,9 +779,9 @@ class inc_sat_solver : public solver {
             }
         }
         catch (tactic_exception & ex) {
-            IF_VERBOSE(1, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
-            set_reason_unknown(ex.msg());
-            TRACE("sat", tout << "exception: " << ex.msg() << "\n";);
+            IF_VERBOSE(1, verbose_stream() << "exception in tactic " << ex.what() << "\n";);
+            set_reason_unknown(ex.what());
+            TRACE("sat", tout << "exception: " << ex.what() << "\n";);
             m_preprocess = nullptr;
             m_bb_rewriter = nullptr;
             return l_undef;
diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp
index e21b0996ff8..44fe15f33d2 100644
--- a/src/sat/sat_solver/sat_smt_solver.cpp
+++ b/src/sat/sat_solver/sat_smt_solver.cpp
@@ -183,9 +183,9 @@ class sat_smt_solver : public solver {
             r = m_solver.check(m_dep.m_literals);
         }
         catch (z3_exception& ex) {
-            IF_VERBOSE(1, verbose_stream() << "exception: " << ex.msg() << "\n";);
+            IF_VERBOSE(1, verbose_stream() << "exception: " << ex.what() << "\n";);
             if (m.inc()) {
-                set_reason_unknown(std::string("(sat.giveup ") + ex.msg() + ')');
+                set_reason_unknown(std::string("(sat.giveup ") + ex.what() + ')');
                 return l_undef;
             }
             r = l_undef;            
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index d43442ed9c4..10711d0bdd4 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -243,12 +243,12 @@ class sat_tactic : public tactic {
         }
         catch (sat::solver_exception & ex) {
             proc.m_solver->collect_statistics(m_stats);
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
         catch (z3_exception& ex) {
             (void)ex;
             proc.m_solver->collect_statistics(m_stats);
-            TRACE("sat", tout << ex.msg() << "\n";);            
+            TRACE("sat", tout << ex.what() << "\n";);            
             throw;
         }
         TRACE("sat_stats", m_stats.display_smt2(tout););
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 26325d3d0a2..1aada6c41f2 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -416,7 +416,7 @@ int STD_CALL main(int argc, char ** argv) {
     }
     catch (z3_exception & ex) {
         // unhandled exception
-        std::cerr << "ERROR: " << ex.msg() << "\n";
+        std::cerr << "ERROR: " << ex.what() << "\n";
         if (ex.has_error_code())
             return ex.error_code();
         else
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index c02d4ef034d..8813ed4bdb3 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -134,7 +134,7 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
         }
     }
     catch (z3_exception & ex) {
-        std::cerr << ex.msg() << "\n";
+        std::cerr << ex.what() << "\n";
     }
     display_statistics();
     display_model();
diff --git a/src/shell/z3_log_frontend.cpp b/src/shell/z3_log_frontend.cpp
index 4a0ce2c3ec6..86813ff2c49 100644
--- a/src/shell/z3_log_frontend.cpp
+++ b/src/shell/z3_log_frontend.cpp
@@ -31,7 +31,7 @@ static void solve(char const * stream_name, std::istream & in) {
         r.parse();
     }
     catch (z3_exception & ex) {
-        std::cerr << "Error at line " << r.get_line() << ": " << ex.msg() << std::endl;
+        std::cerr << "Error at line " << r.get_line() << ": " << ex.what() << std::endl;
     }
     clock_t end_time = clock();
     memory::display_max_usage(std::cout);
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index f79f7851f5c..85100cb0963 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -96,7 +96,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
     }
     catch (model_evaluator_exception & ex) {
         (void)ex;
-        TRACE("model_evaluator", tout << ex.msg() << "\n";);
+        TRACE("model_evaluator", tout << ex.what() << "\n";);
         return false;
     }
 }
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index ccbefa69e3c..c8958c61cae 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -198,7 +198,7 @@ namespace smt {
             }
             catch (z3_exception & ex) {
                 if (finished_id == UINT_MAX) {
-                    ex_msg = ex.msg();
+                    ex_msg = ex.what();
                     ex_kind = DEFAULT_EX;
                     done = true;
                 }
diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index 89b2b713566..0914df13fb0 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -310,7 +310,7 @@ class smt_tactic : public tactic {
             }
         }
         catch (rewriter_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
 
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index b1fe47b6574..8310de5618d 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -959,7 +959,7 @@ namespace smt {
             return internalize_term_core(term);
         }
         catch (z3_exception& ex) {
-            IF_VERBOSE(1, verbose_stream() << "internalize_term: " << ex.msg() << "\n";);
+            IF_VERBOSE(1, verbose_stream() << "internalize_term: " << ex.what() << "\n";);
             throw;
         }
     }
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 34d31ec84de..e2a2f20115e 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -202,7 +202,7 @@ class combined_solver : public solver {
                 throw;
             }
             else {
-                set_reason_unknown(ex.msg());
+                set_reason_unknown(ex.what());
             }
         }
         return l_undef;
diff --git a/src/solver/parallel_tactical.cpp b/src/solver/parallel_tactical.cpp
index f748379b1c9..068dc03043e 100644
--- a/src/solver/parallel_tactical.cpp
+++ b/src/solver/parallel_tactical.cpp
@@ -710,7 +710,7 @@ class parallel_tactic : public tactic {
             }
         }
         catch (z3_exception& ex) {   
-            IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";);
+            IF_VERBOSE(1, verbose_stream() << ex.what() << "\n";);
             if (m_queue.in_shutdown()) return;
             m_queue.shutdown();
             std::lock_guard<std::mutex> lock(m_mutex);
@@ -718,7 +718,7 @@ class parallel_tactic : public tactic {
                 m_exn_code = ex.error_code();
             }
             else {
-                m_exn_msg = ex.msg();
+                m_exn_msg = ex.what();
                 m_exn_code = -1;
             }
         }
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index bf05554affc..8437f92ccf9 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -95,7 +95,7 @@ lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector cons
             return l_undef;
         }
         else {
-            set_reason_unknown(ex.msg());
+            set_reason_unknown(ex.what());
         }
         throw;
     }
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index cdabecb2753..dfdae5e5aeb 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -1,5 +1,4 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
+/*++ Copyright (c) 2012 Microsoft Corporation
 
 Module Name:
 
@@ -270,14 +269,14 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
 
     }
     catch (z3_error & ex) {
-        TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
+        TRACE("tactic2solver", tout << "exception: " << ex.what() << "\n";);
         m_result->m_proof = pr;
         throw ex;
     }
     catch (z3_exception & ex) {
-        TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
+        TRACE("tactic2solver", tout << "exception: " << ex.what() << "\n";);
         m_result->set_status(l_undef);
-        m_result->m_unknown = ex.msg();
+        m_result->m_unknown = ex.what();
         m_result->m_proof = pr;
     }
     m_tactic->collect_statistics(m_result->m_stats);
diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp
index 565f43af9c6..1060a0d96a7 100644
--- a/src/tactic/arith/factor_tactic.cpp
+++ b/src/tactic/arith/factor_tactic.cpp
@@ -316,7 +316,7 @@ class factor_tactic : public tactic {
             throw ex;
         }
         catch (z3_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
 
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index c96ca749b90..71bcf1391a2 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -317,7 +317,7 @@ class fix_dl_var_tactic : public tactic {
             (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
     
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index 450a7d25a93..93b8ddbcae9 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -325,7 +325,7 @@ class lia2pb_tactic : public tactic {
             (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
     
diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp
index 7c09703eba3..8898ab6132e 100644
--- a/src/tactic/arith/normalize_bounds_tactic.cpp
+++ b/src/tactic/arith/normalize_bounds_tactic.cpp
@@ -169,7 +169,7 @@ class normalize_bounds_tactic : public tactic {
             (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
     
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 40ee967ba8c..cc04dae939c 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -937,7 +937,7 @@ class purify_arith_tactic : public tactic {
             result.push_back(g.get());
         }
         catch (rewriter_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
     
diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp
index 623f82cf9d6..284aeeabed0 100644
--- a/src/tactic/arith/recover_01_tactic.cpp
+++ b/src/tactic/arith/recover_01_tactic.cpp
@@ -416,7 +416,7 @@ class recover_01_tactic : public tactic {
             (*m_imp)(g, result);
         }
         catch (rewriter_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
     
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 5e35d7d9ad0..0fd20313de1 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -141,7 +141,7 @@ class bit_blaster_tactic : public tactic {
             (*m_imp)(g, result);
         }
         catch (rewriter_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
 
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 5d5bc09454b..55615f3b6ab 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -238,7 +238,7 @@ class propagate_values_tactic : public tactic {
             run(in, result);
         }
         catch (rewriter_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
     
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index 6e2068e26e2..27e859196df 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -98,7 +98,7 @@ void simplify_tactic::operator()(goal_ref const & in,
         m_clean = false;
     }
     catch (rewriter_exception & ex) {
-        throw tactic_exception(ex.msg());
+        throw tactic_exception(ex.what());
     }
 }
 
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index 79c1993b211..fc1cf2b4f12 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -129,7 +129,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
                 m_simp->reduce();
         }
         catch (rewriter_exception& ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
         m_goal->elim_true();
         m_goal->elim_redundancies();
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 2824392280a..bc9825171f0 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -136,7 +136,7 @@ class fpa2bv_tactic : public tactic {
             (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
-            throw tactic_exception(ex.msg());
+            throw tactic_exception(ex.what());
         }
     }
 
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 36dc5d4d037..ad296c9859e 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -196,7 +196,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result) {
         t.cleanup();
     }
     catch (tactic_exception & ex) {
-        IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(tactic-exception \"" << escaped(ex.msg()) << "\")\n");
+        IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(tactic-exception \"" << escaped(ex.what()) << "\")\n");
         t.cleanup();
         throw ex;
     }
@@ -215,7 +215,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
         exec(t, g, r);
     }
     catch (z3_exception & ex) {
-        reason_unknown = ex.msg();
+        reason_unknown = ex.what();
         if (r.size() > 0) pr = r[0]->pr(0);
         return l_undef;
     }
diff --git a/src/tactic/tactic_exception.h b/src/tactic/tactic_exception.h
index c6be82daabb..95121c5d017 100644
--- a/src/tactic/tactic_exception.h
+++ b/src/tactic/tactic_exception.h
@@ -26,7 +26,7 @@ class tactic_exception : public z3_exception {
     std::string m_msg;
 public:
     tactic_exception(std::string && msg) : m_msg(std::move(msg)) {}
-    char const * msg() const override { return m_msg.c_str(); }
+    char const * what() const override { return m_msg.c_str(); }
 };
 
 #define TACTIC_CANCELED_MSG      Z3_CANCELED_MSG
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 78e15aef7a7..1ae8271c99f 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -362,7 +362,7 @@ class or_else_tactical : public nary_tactical {
                     throw;
                 }
                 catch (z3_exception& ex) {
-                    IF_VERBOSE(10, verbose_stream() << ex.msg() << " in or-else\n");
+                    IF_VERBOSE(10, verbose_stream() << ex.what() << " in or-else\n");
                     throw;
                 }
                 catch (const std::exception &ex) {
@@ -546,7 +546,7 @@ class par_tactical : public or_else_tactical {
             catch (tactic_exception & ex) {
                 if (i == 0) {
                     ex_kind = TACTIC_EX;
-                    ex_msg = ex.msg();
+                    ex_msg = ex.what();
                 }
             }
             catch (z3_error & err) {
@@ -558,7 +558,7 @@ class par_tactical : public or_else_tactical {
             catch (z3_exception & z3_ex) {
                 if (i == 0) {
                     ex_kind = DEFAULT_EX;
-                    ex_msg = z3_ex.msg();
+                    ex_msg = z3_ex.what();
                 }
             }
         };
@@ -703,7 +703,7 @@ class par_and_then_tactical : public and_then_tactical {
                             curr_failed = true;
                             failed      = true;
                             ex_kind     = TACTIC_EX;
-                            ex_msg      = ex.msg();
+                            ex_msg      = ex.what();
                         }
                     }
                 }
@@ -725,7 +725,7 @@ class par_and_then_tactical : public and_then_tactical {
                             curr_failed = true;
                             failed      = true;
                             ex_kind     = DEFAULT_EX;
-                            ex_msg      = z3_ex.msg();
+                            ex_msg      = z3_ex.what();
                         }
                     }
                 }
diff --git a/src/test/ex.cpp b/src/test/ex.cpp
index 10b5f8a90e9..829386112eb 100644
--- a/src/test/ex.cpp
+++ b/src/test/ex.cpp
@@ -19,24 +19,23 @@ Revision History:
 #include<iostream>
 #include "util/z3_exception.h"
 
-class ex {
+class ex : public std::exception {
 public:
     virtual ~ex() = default;
-    virtual char const * msg() const = 0;
 };
 
 class ex1 : public ex {
     char const * m_msg;
 public:
     ex1(char const * m):m_msg(m) {}
-    char const * msg() const override { return m_msg; }
+    char const * what() const override { return m_msg; }
 };
 
 class ex2 : public ex {
     std::string m_msg;
 public:
     ex2(char const * m):m_msg(m) {}
-    char const * msg() const override { return m_msg.c_str(); }
+    char const * what() const override { return m_msg.c_str(); }
 };
 
 static void th() {
@@ -48,7 +47,7 @@ static void tst1() {
         th();
     }
     catch (ex & e) {
-        std::cerr << e.msg() << "\n";
+        std::cerr << e.what() << "\n";
     }
 }
 
@@ -57,7 +56,7 @@ static void tst2() {
         throw default_exception(default_exception::fmt(), "Format %d %s", 12, "twelve");
     }
     catch (z3_exception& ex) {
-        std::cerr << ex.msg() << "\n";
+        std::cerr << ex.what() << "\n";
     }
 }
 
diff --git a/src/test/main.cpp b/src/test/main.cpp
index f028d6ceb35..c05af0aa299 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -134,7 +134,7 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t
                 gparams::set(key, value);
             }
             catch (z3_exception& ex) {
-                std::cerr << ex.msg() << "\n";
+                std::cerr << ex.what() << "\n";
             }
         }
         i++;
diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp
index b03cc5f2ecf..75b23be3d8b 100644
--- a/src/test/mpff.cpp
+++ b/src/test/mpff.cpp
@@ -38,7 +38,7 @@ static void tst1() {
         }
     }
     catch (const z3_exception & ex) {
-        std::cout << ex.msg() << "\n";
+        std::cout << ex.what() << "\n";
     }
 }
 
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index 91e6076793f..79fc5ff43aa 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -926,6 +926,6 @@ void tst_udoc_relation() {
         tester.test1();
     }
     catch (z3_exception& ex) {
-        std::cout << ex.msg() << "\n";
+        std::cout << ex.what() << "\n";
     }
 }
diff --git a/src/test/vector.cpp b/src/test/vector.cpp
index fe0b50ddbc6..c9bf5a75a65 100644
--- a/src/test/vector.cpp
+++ b/src/test/vector.cpp
@@ -50,7 +50,7 @@ static void tst1() {
             v1.resize(i);
         }
         catch (z3_exception& e) {
-            std::cout << e.msg() << "\n";
+            std::cout << e.what() << "\n";
             break;
         }
         i *= 2;
diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h
index 31ef5bdd6a9..5d2e0953e37 100644
--- a/src/util/checked_int64.h
+++ b/src/util/checked_int64.h
@@ -29,7 +29,7 @@ Revision History:
 
 
 class overflow_exception : public z3_exception {
-    char const* msg() const override { return "checked_int64 overflow/underflow"; }
+    char const* what() const override { return "checked_int64 overflow/underflow"; }
 };
 
 template<bool CHECK>
@@ -364,4 +364,4 @@ inline checked_int64<CHECK> gcd(checked_int64<CHECK> const& a, checked_int64<CHE
         lasty = temp;
     }
     return _a;
-}
\ No newline at end of file
+}
diff --git a/src/util/mpff.h b/src/util/mpff.h
index 254c52572c5..d74785f4465 100644
--- a/src/util/mpff.h
+++ b/src/util/mpff.h
@@ -182,15 +182,15 @@ class mpff_manager {
     static bool field() { return true; }
 
     class exception : public z3_exception {
-        char const * msg() const override { return "multi-precision floating point (mpff) exception"; }
+        char const * what() const override { return "multi-precision floating point (mpff) exception"; }
     };
     
     class overflow_exception : public exception {
-        char const * msg() const override { return "multi-precision floating point (mpff) overflow"; }
+        char const * what() const override { return "multi-precision floating point (mpff) overflow"; }
     };
 
     class div0_exception : public exception {
-        char const * msg() const override { return "multi-precision floating point (mpff) division by zero"; }
+        char const * what() const override { return "multi-precision floating point (mpff) division by zero"; }
     };
     
     mpff_manager(unsigned prec = 2, unsigned initial_capacity = 1024);
diff --git a/src/util/mpfx.h b/src/util/mpfx.h
index c563c287232..f18ac3ee71f 100644
--- a/src/util/mpfx.h
+++ b/src/util/mpfx.h
@@ -129,15 +129,15 @@ class mpfx_manager {
     static bool field() { return true; }
 
     class exception : public z3_exception {
-        char const * msg() const override { return "multi-precision fixed point (mpfx) exception"; }
+        char const * what() const override { return "multi-precision fixed point (mpfx) exception"; }
     };
     
     class overflow_exception : public exception {
-        char const * msg() const override { return "multi-precision fixed point (mpfx) overflow"; }
+        char const * what() const override { return "multi-precision fixed point (mpfx) overflow"; }
     };
     
     class div0_exception : public exception {
-        char const * msg() const override { return "multi-precision fixed point (mpfx) division by zero"; }
+        char const * what() const override { return "multi-precision fixed point (mpfx) division by zero"; }
     };
 
     mpfx_manager(unsigned int_sz = 2, unsigned frac_sz = 1, unsigned initial_capacity = 1024);
diff --git a/src/util/z3_exception.cpp b/src/util/z3_exception.cpp
index ae3f321cbcb..8c08308ae58 100644
--- a/src/util/z3_exception.cpp
+++ b/src/util/z3_exception.cpp
@@ -35,7 +35,7 @@ z3_error::z3_error(unsigned error_code):m_error_code(error_code) {
     SASSERT(error_code != 0); 
 }
 
-char const * z3_error::msg() const {
+char const * z3_error::what() const {
     switch (m_error_code) {
     case ERR_MEMOUT: return "out of memory";
     case ERR_TIMEOUT: return "timeout";
@@ -67,6 +67,6 @@ default_exception::default_exception(fmt, char const* msg, ...) {
     m_msg = out.str();
 }
 
-char const * default_exception::msg() const { 
+char const * default_exception::what() const { 
     return m_msg.c_str(); 
 }
diff --git a/src/util/z3_exception.h b/src/util/z3_exception.h
index b6875257c79..a31ac89cd42 100644
--- a/src/util/z3_exception.h
+++ b/src/util/z3_exception.h
@@ -19,11 +19,11 @@ Module Name:
 #pragma once
 
 #include<string>
+#include<exception>
 
-class z3_exception {
+class z3_exception : public std::exception {
 public:
     virtual ~z3_exception() = default;
-    virtual char const * msg() const = 0;
     virtual unsigned error_code() const;
     bool has_error_code() const;
 };
@@ -32,7 +32,7 @@ class z3_error : public z3_exception {
     unsigned m_error_code;
 public:
     z3_error(unsigned error_code);
-    char const * msg() const override;
+    char const * what() const override;
     unsigned error_code() const override;
 };
 
@@ -42,6 +42,6 @@ class default_exception : public z3_exception {
     struct fmt {};
     default_exception(std::string && msg) : m_msg(std::move(msg)) {}
     default_exception(fmt, char const* msg, ...);
-    char const * msg() const override;
+    char const * what() const override;
 };