diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index e5ab4a8066c..03c726698fe 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -277,7 +277,7 @@ namespace datatype {
         }
 
 
-        struct invalid_datatype {};
+        struct invalid_datatype : public std::exception {};
 
         sort * plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
             try {
diff --git a/src/ast/substitution/demodulator_rewriter.cpp b/src/ast/substitution/demodulator_rewriter.cpp
index f174b149186..6e7ac996c5b 100644
--- a/src/ast/substitution/demodulator_rewriter.cpp
+++ b/src/ast/substitution/demodulator_rewriter.cpp
@@ -828,7 +828,7 @@ bool demodulator_match_subst::can_rewrite(expr* n, expr* lhs) {
 */
 struct match_args_aux_proc {
     substitution &                               m_subst;
-    struct no_match {};
+    struct no_match : public std::exception {};
 
     match_args_aux_proc(substitution & s):m_subst(s) {}
 
diff --git a/src/parsers/util/simple_parser.h b/src/parsers/util/simple_parser.h
index c3cc0712e0f..7601b1606ed 100644
--- a/src/parsers/util/simple_parser.h
+++ b/src/parsers/util/simple_parser.h
@@ -29,7 +29,7 @@ class scanner;
 */
 class simple_parser {
 protected:
-    struct parser_error {};
+    struct parser_error : public std::exception {};
     struct builtin_op {
         family_id m_family_id;
         decl_kind m_kind;
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 325f343b467..cfd86371147 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -2456,7 +2456,7 @@ namespace qe {
     }
 
     bool has_quantified_uninterpreted(ast_manager& m, expr* fml) {
-        struct found {};
+        struct found : public std::exception {};
         struct proc {
             ast_manager& m;
             proc(ast_manager& m):m(m) {}
diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h
index 3ca8102ffb2..f6be01ef822 100644
--- a/src/sat/dimacs.h
+++ b/src/sat/dimacs.h
@@ -26,7 +26,7 @@ Revision History:
 bool parse_dimacs(std::istream & s, std::ostream& err, sat::solver & solver);
 
 namespace dimacs {
-    struct lex_error {};
+    struct lex_error : public std::exception {};
 
     class stream_buffer {
         std::istream & m_stream;
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 657c92178bd..2a150f4d9a1 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -90,7 +90,7 @@ namespace sat {
     
     class solver : public solver_core {
     public:
-        struct abort_solver {};
+        struct abort_solver : public std::exception {};
     protected:
         enum search_state { s_sat, s_unsat };
 
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 7a567d5a94b..3a984caf2dc 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -147,7 +147,7 @@ namespace smt {
                 return m_inv;
             }
 
-            struct is_model_value {};
+            struct is_model_value : public std::exception {};
             void operator()(expr* n) {
                 if (m.is_model_value(n)) {
                     throw is_model_value();
@@ -540,7 +540,7 @@ namespace smt {
                 return !contains_array(e);
             }
 
-            struct found_array {};
+            struct found_array : public std::exception {};
             expr_mark m_visited;
             void operator()(expr* n) {
                 if (m_array.is_array(n))
diff --git a/src/solver/check_logic.cpp b/src/solver/check_logic.cpp
index 36c08c4d590..308ceae3076 100644
--- a/src/solver/check_logic.cpp
+++ b/src/solver/check_logic.cpp
@@ -215,7 +215,7 @@ struct check_logic::imp {
         m_logic = logic;
     }
 
-    struct failed {};
+    struct failed : public std::exception {};
     std::string m_last_error;
 
     void fail(std::string &&msg) {
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index 71bcf1391a2..30e145ccb61 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -32,7 +32,7 @@ Revision History:
 class fix_dl_var_tactic : public tactic {
 
     struct is_target {
-        struct failed {};
+        struct failed : public std::exception {};
         ast_manager &          m;
         arith_util &           m_util;
         expr_fast_mark1 *      m_visited = nullptr;
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index 93b8ddbcae9..aa738ede08c 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -86,7 +86,7 @@ class lia2pb_tactic : public tactic {
             return is_target_core(n, u) && u > rational(1);
         }
         
-        struct failed {};
+        struct failed : public std::exception {};
 
         struct visitor {
             imp & m_owner;
diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp
index d3f19d1bdd3..090bd3e48c5 100644
--- a/src/tactic/bv/bv1_blaster_tactic.cpp
+++ b/src/tactic/bv/bv1_blaster_tactic.cpp
@@ -338,7 +338,7 @@ class bv1_blaster_tactic : public tactic {
             m_rw(m, p) {
         }
 
-        struct not_target {};
+        struct not_target : public std::exception {};
         
         struct visitor {
             family_id m_bv_fid;