Throw appropriate exceptions when converting constraints

NathanJPhillips · Apr 25, 2018 · 89cf6fe · 89cf6fe
1 parent 2ae66c2
commit 89cf6fe
Showing 1 changed file with 13 additions and 4 deletions.
diff --git 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));
+        }
+      }
     }
   }
 }