diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 37bedbed2f4..e9bae06e545 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -705,10 +705,10 @@ int bmct::do_language_agnostic_bmc(
     message.error() << error_msg << message.eom;
     return CPROVER_EXIT_EXCEPTION;
   }
-  catch(...)
+  catch(std::runtime_error &e)
   {
-    message.error() << "unable to get solver" << message.eom;
-    throw std::current_exception();
+    message.error() << e.what() << message.eom;
+    return CPROVER_EXIT_EXCEPTION;
   }
 
   switch(result)
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 0d3709dde8e..9554f1fd3a0 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -523,10 +523,19 @@ void symex_target_equationt::convert_constraints(
   {
     if(step.is_constraint())
     {
-      if(step.ignore)
-        continue;
-
-      decision_procedure.set_to_true(step.cond_expr);
+      if(!step.ignore)
+      {
+        try
+        {
+          decision_procedure.set_to_true(step.cond_expr);
+        }
+        catch(const bitvector_conversion_exceptiont &conversion_exception)
+        {
+          util_throw_with_nested(
+            equation_conversion_exceptiont(
+              "Error converting constraints for step", step));
+        }
+      }
     }
   }
 }
diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp
index 8621efa3cbe..2e7ac9aa500 100644
--- a/src/solvers/flattening/boolbv_equality.cpp
+++ b/src/solvers/flattening/boolbv_equality.cpp
@@ -12,16 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_type.h>
 #include <util/invariant.h>
 
+#include "bv_conversion_exceptions.h"
 #include "flatten_byte_operators.h"
 
 literalt boolbvt::convert_equality(const equal_exprt &expr)
 {
   const bool is_base_type_eq =
     base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
-  DATA_INVARIANT(
-    is_base_type_eq,
-    std::string("equality without matching types:\n") + "######### lhs: " +
-      expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty());
+  if(!is_base_type_eq)
+  {
+    const std::string error_msg =
+      std::string("equality without matching types:\n") + "######### lhs: " +
+      expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty();
+    throw bitvector_conversion_exceptiont(error_msg, expr);
+  }
 
   // see if it is an unbounded array
   if(is_unbounded_array(expr.lhs().type()))