SMT2 backend: type2id can now do union_tag

kroening · kroening · commit 2b7ff7da5f50 · 2022-05-25T17:35:06.000+01:00
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -944,6 +944,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());

Original file line number	Diff line number	Diff line change
`@@ -944,6 +944,10 @@ std::string smt2_convt::type2id(const typet &type) const`
`944`	`944`	`else`
`945`	`945`	`return "S" + std::to_string(boolbv_width(type));`
`946`	`946`	`}`
	`947`	`+ else if(type.id() == ID_union_tag)`
	`948`	`+ {`
	`949`	`+ return "U" + std::to_string(boolbv_width(type));`
	`950`	`+ }`
`947`	`951`	`else if(type.id() == ID_array)`
`948`	`952`	`{`
`949`	`953`	`return "A" + type2id(to_array_type(type).element_type());`