SMT2 backend: type2id can now do union_tag

The SMT2 backend constructs strings to disambiguate overloaded operations
using types, and now supports generating strings for union_tag types.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -996,6 +996,10 @@ std::string smt2_convt::type2id(const typet &type) const
     else
       return "S" + std::to_string(boolbv_width(type));
   }
+  else if(type.id() == ID_union_tag)
+  {
+    return "U" + std::to_string(boolbv_width(type));
+  }
   else if(type.id() == ID_array)
   {
     return "A" + type2id(to_array_type(type).element_type());