Remove clashing parts of my previous implementation.

Author: martin

src/solvers/smt2/smt2_conv.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ieee_float.h>
 #include <util/base_type.h>
 #include <util/string2int.h>
+#include <util/invariant.h>
 
 #include <ansi-c/string_constant.h>
 
@@ -34,7 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // Mark different kinds of error condition
 // General
-#define UNREACHABLE throw "Supposidly unreachable location reached"
 #define PARSERERROR(S) throw S
 
 // Error checking the expression type
@@ -45,7 +45,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define UNEXPECTEDCASE(S) throw "Unexpected case: " S
 
 // General todos
-#define TODO(S) throw "TODO: " S
+#define SMT2_TODO(S) throw "TODO: " S
 
 void smt2_convt::print_assignment(std::ostream &out) const
 {
@@ -952,7 +952,7 @@ void smt2_convt::convert_expr(const exprt &expr)
         out << "))"; // mk-, let
       }
       else
-        TODO("bitnot for vectors");
+        SMT2_TODO("bitnot for vectors");
     }
     else
     {
@@ -1017,7 +1017,7 @@ void smt2_convt::convert_expr(const exprt &expr)
         out << "))"; // mk-, let
       }
       else
-        TODO("unary minus for vector");
+        SMT2_TODO("unary minus for vector");
     }
     else
     {
@@ -1363,7 +1363,7 @@ void smt2_convt::convert_expr(const exprt &expr)
     assert(expr.operands().size()==1);
 
     out << "false"; // TODO
-    TODO("pointer_object_has_type not implemented");
+    SMT2_TODO("pointer_object_has_type not implemented");
   }
   else if(expr.id()==ID_string_constant)
   {
@@ -1432,7 +1432,7 @@ void smt2_convt::convert_expr(const exprt &expr)
       convert_expr(tmp);
       out << ")) bin1)"; // bvlshr, extract, =
       #endif
-      TODO("smt2: extractbits with non-constant index");
+      SMT2_TODO("smt2: extractbits with non-constant index");
     }
   }
   else if(expr.id()==ID_replication)
@@ -1944,7 +1944,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
           // This conversion is non-trivial as it requires creating a
           // new bit-vector variable and then asserting that it converts
           // to the required floating-point number.
-          TODO("bit-wise floatbv to bv");
+          SMT2_TODO("bit-wise floatbv to bv");
         }
         else
         {
@@ -2017,7 +2017,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
         out << "(_ bv" << i << " " << to_width << ")";
       }
       else
-        TODO("can't convert non-constant integer to bitvector");
+        SMT2_TODO("can't convert non-constant integer to bitvector");
     }
     else if(src_type.id()==ID_struct) // flatten a struct to a bit-vector
     {
@@ -2207,7 +2207,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
   }
   else if(dest_type.id()==ID_range)
   {
-    TODO("range typecast");
+    SMT2_TODO("range typecast");
   }
   else if(dest_type.id()==ID_floatbv)
   {
@@ -3031,11 +3031,11 @@ void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr)
     }
     else if(type.id()==ID_complex)
     {
-      TODO("+ for floatbv complex");
+      SMT2_TODO("+ for floatbv complex");
     }
     else if(type.id()==ID_vector)
     {
-      TODO("+ for floatbv vector");
+      SMT2_TODO("+ for floatbv vector");
     }
     else
       UNEXPECTEDCASE("unsupported type for +: "+type.id_string());
@@ -3093,7 +3093,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
   }
   else if(expr.type().id()==ID_pointer)
   {
-    TODO("pointer subtraction");
+    SMT2_TODO("pointer subtraction");
   }
   else if(expr.type().id()==ID_vector)
   {
@@ -3527,7 +3527,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
     typecast_exprt index_tc(index, expr_type);
 
     // TODO: SMT2-ify
-    TODO("SMT2-ify");
+    SMT2_TODO("SMT2-ify");
     out << "(bvor ";
     out << "(band ";
 
@@ -3565,7 +3565,7 @@ void smt2_convt::convert_update(const exprt &expr)
 {
   assert(expr.operands().size()==3);
 
-  TODO("smt2_convt::convert_update to be implemented");
+  SMT2_TODO("smt2_convt::convert_update to be implemented");
 }
 
 void smt2_convt::convert_index(const index_exprt &expr)
@@ -3651,7 +3651,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
       mp_integer index_int;
       if(to_integer(expr.index(), index_int))
       {
-        TODO("non-constant index on vectors");
+        SMT2_TODO("non-constant index on vectors");
       }
       else
       {
@@ -3662,7 +3662,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
     }
     else
     {
-      TODO("index on vectors");
+      SMT2_TODO("index on vectors");
     }
   }
   else