diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index 3d9f0bd25..75db906a1 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -22,7 +22,7 @@ Revision History:
 #include "ast/simplifiers/bound_manager.h"
 
 struct is_unbounded_proc {
-    struct found {};
+    struct found : public std::exception {};
     arith_util      m_util;
     bound_manager & m_bm;
     
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 507a54b6a..5b1c4831f 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -35,7 +35,7 @@ Notes:
 
 class pb2bv_tactic : public tactic {
 public:
-    struct non_pb { expr* e; non_pb(expr* e) : e(e) {}};
+    struct non_pb : public std::exception { expr* e; non_pb(expr* e) : e(e) {}};
 
     struct only_01_visitor {
         typedef rational numeral;
@@ -167,7 +167,7 @@ private:
 
         enum constraint_kind { EQ, GE, LE };
 
-        struct failed {};
+        struct failed : public std::exception {};
 
         struct visitor {
             imp & m_owner;
diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp
index 179bd6473..21498f08f 100644
--- a/src/tactic/arith/probe_arith.cpp
+++ b/src/tactic/arith/probe_arith.cpp
@@ -130,7 +130,7 @@ public:
 };
 
 struct has_nlmul {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager& m;
     arith_util   a;
     has_nlmul(ast_manager& m):m(m), a(m) {}
@@ -185,7 +185,7 @@ probe * mk_arith_max_bw_probe() {
 
 namespace {
 struct is_non_qflira_functor {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     arith_util    u;
     bool          m_int;
@@ -240,7 +240,7 @@ struct is_non_qflira_functor {
 };
 
 struct is_non_qfauflira_functor {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     arith_util    m_arith_util;
     array_util    m_array_util;
@@ -427,7 +427,7 @@ probe * mk_is_mip_probe() {
 namespace {
 
 struct is_non_nira_functor {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     arith_util    u;
     bool          m_int;
@@ -572,7 +572,7 @@ static bool is_lira(goal const & g) {
 
 
 struct is_non_qfufnra_functor {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     arith_util    u;
     bool          m_has_nonlinear;
diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index 9595cc606..fbac861d8 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -32,7 +32,7 @@ Notes:
 
 
 struct is_non_fp_qfnra_predicate {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     bv_util       bu;
     fpa_util      fu;
diff --git a/src/tactic/fpa/qffplra_tactic.cpp b/src/tactic/fpa/qffplra_tactic.cpp
index 711eadc8f..a4d8b5e26 100644
--- a/src/tactic/fpa/qffplra_tactic.cpp
+++ b/src/tactic/fpa/qffplra_tactic.cpp
@@ -27,7 +27,7 @@ tactic * mk_qffplra_tactic(ast_manager & m, params_ref const & p) {
 }
 
 struct is_fpa_function {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     fpa_util      fu;
     
diff --git a/src/tactic/goal_util.cpp b/src/tactic/goal_util.cpp
index 965860cf9..065a198b3 100644
--- a/src/tactic/goal_util.cpp
+++ b/src/tactic/goal_util.cpp
@@ -20,7 +20,7 @@ Revision History:
 #include "tactic/goal.h"
 
 struct has_term_ite_functor {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     has_term_ite_functor(ast_manager & _m):m(_m) {}
     void operator()(var *) {}
diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp
index fe813c28f..263e77813 100644
--- a/src/tactic/probe.cpp
+++ b/src/tactic/probe.cpp
@@ -248,7 +248,7 @@ probe * mk_div(probe * p1, probe * p2) {
 }
 
 struct is_non_propositional_predicate {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
 
     is_non_propositional_predicate(ast_manager & _m):m(_m) {}
@@ -270,7 +270,7 @@ struct is_non_propositional_predicate {
 };
 
 struct is_non_qfbv_predicate {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     bv_util       u;
 
@@ -325,7 +325,7 @@ probe * mk_is_qfbv_probe() {
 }
 
 struct is_non_qfaufbv_predicate {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     bv_util       m_bv_util;
     array_util    m_array_util;
@@ -364,7 +364,7 @@ probe * mk_is_qfaufbv_probe() {
 
 
 struct is_non_qfufbv_predicate {
-    struct found {};
+    struct found : public std::exception {};
     ast_manager & m;
     bv_util       m_bv_util;
 
@@ -503,7 +503,7 @@ probe * mk_produce_unsat_cores_probe() {
 }
 
 struct has_pattern_probe : public probe {
-    struct found {};
+    struct found : public std::exception {};
 
     struct proc {
         void operator()(var * n) {}
@@ -536,7 +536,7 @@ probe * mk_has_pattern_probe() {
 
 
 struct has_quantifier_probe : public probe {
-    struct found {};
+    struct found : public std::exception {};
 
     struct proc {
         void operator()(var * n) {}