diff --git a/rumur/src/main.cc b/rumur/src/main.cc
index dc697a2f..7b2b4b3a 100644
--- a/rumur/src/main.cc
+++ b/rumur/src/main.cc
@@ -569,8 +569,8 @@ int main(int argc, char **argv) {
       smt::simplify(*m);
     } catch (smt::BudgetExhausted&) {
       *info << "SMT solver budget (" << options.smt.budget << "ms) exhausted\n";
-    } catch (smt::Unsupported&) {
-      *info << "SMT solver encountered an unsupported expression\n";
+    } catch (smt::Unsupported &e) {
+      *info << e.what() << "\n";
     }
   }
 
diff --git a/rumur/src/smt/except.h b/rumur/src/smt/except.h
index e4d458ca..8d654830 100644
--- a/rumur/src/smt/except.h
+++ b/rumur/src/smt/except.h
@@ -4,6 +4,7 @@
 
 #include <cstddef>
 #include <stdexcept>
+#include <string>
 
 namespace smt {
 
@@ -15,7 +16,10 @@ class BudgetExhausted : public std::runtime_error {
 class Unsupported : public std::runtime_error {
  public:
   Unsupported(): std::runtime_error("part of an expression was outside the "
-    "currently implemented functionality") { }
+    "currently implemented SMT functionality") { }
+
+  Unsupported(const std::string &expr): std::runtime_error("SMT solver "
+    "encountered unsupported expression \"" + expr + "\"") { }
 };
 
 }
diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc
index 4ea3aa0c..31c3af4e 100644
--- a/rumur/src/smt/simplify.cc
+++ b/rumur/src/smt/simplify.cc
@@ -105,7 +105,7 @@ namespace { class Simplifier : public BaseTraversal {
     if (n == *Boolean)
       return;
 
-    throw Unsupported();
+    throw Unsupported(n.to_string());
   }
 
   void visit_eq(Eq &n) final { visit_bexpr(n); }
diff --git a/rumur/src/smt/translate.cc b/rumur/src/smt/translate.cc
index c7f4c812..ed0211f9 100644
--- a/rumur/src/smt/translate.cc
+++ b/rumur/src/smt/translate.cc
@@ -37,8 +37,8 @@ namespace { class Translator : public ConstExprTraversal {
     *this << "(and " << *n.lhs << " " << *n.rhs << ")";
   }
 
-  void visit_element(const Element&) {
-    throw Unsupported();
+  void visit_element(const Element &n) {
+    throw Unsupported(n.to_string());
   }
 
   void visit_exprid(const ExprID &n) {
@@ -49,24 +49,24 @@ namespace { class Translator : public ConstExprTraversal {
     *this << "(= " << *n.lhs << " " << *n.rhs << ")";
   }
 
-  void visit_exists(const Exists&) {
-    throw Unsupported();
+  void visit_exists(const Exists &n) {
+    throw Unsupported(n.to_string());
   }
 
   void visit_div(const Div &n) {
     *this << "(div " << *n.lhs << " " << *n.rhs << ")";
   }
 
-  void visit_field(const Field&) {
-    throw Unsupported();
+  void visit_field(const Field &n) {
+    throw Unsupported(n.to_string());
   }
 
-  void visit_forall(const Forall&) {
-    throw Unsupported();
+  void visit_forall(const Forall &n) {
+    throw Unsupported(n.to_string());
   }
 
-  void visit_functioncall(const FunctionCall&) {
-    throw Unsupported();
+  void visit_functioncall(const FunctionCall &n) {
+    throw Unsupported(n.to_string());
   }
 
   void visit_geq(const Geq &n) {
@@ -81,8 +81,8 @@ namespace { class Translator : public ConstExprTraversal {
     *this << "(=> " << *n.lhs << " " << *n.rhs << ")";
   }
 
-  void visit_isundefined(const IsUndefined&) {
-    throw Unsupported();
+  void visit_isundefined(const IsUndefined &n) {
+    throw Unsupported(n.to_string());
   }
 
   void visit_leq(const Leq &n) {