Introduce formula conversion exception

Author: thk123

src/goto-symex/equation_conversion_exceptions.h

@@ -0,0 +1,52 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Exceptions that can be raised during the equation conversion phase
+
+#ifndef CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
+#define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
+
+#include <ostream>
+#include <util/namespace.h>
+#include "symex_target_equation.h"
+
+class guard_conversion_exceptiont : public std::runtime_error
+{
+public:
+  guard_conversion_exceptiont(
+      const symex_target_equationt::SSA_stept &step,
+      const namespacet &ns) :
+    runtime_error("Error converting guard for step"), step(step)
+  {
+    std::ostringstream error_msg;
+    error_msg << runtime_error::what();
+    error_msg << "\nStep:\n";
+    step.output(ns, error_msg);
+    error_message = error_msg.str();
+  }
+
+  guard_conversion_exceptiont(
+    const symex_target_equationt::SSA_stept &step) :
+    guard_conversion_exceptiont(step, namespacet{symbol_tablet{}})
+  {
+  }
+
+  const char *what() const noexcept override
+  {
+    return error_message.c_str();
+  }
+
+private:
+  symex_target_equationt::SSA_stept step;
+  std::string error_message;
+};
+
+
+
+#endif //CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H

src/goto-symex/symex_target_equation.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/flattening/bv_conversion_exceptions.h>
 
 #include "goto_symex_state.h"
+#include "equation_conversion_exceptions.h"
 
 /// read from a shared variable
 void symex_target_equationt::shared_read(