SMT2 backend: type2id can now do arrays

kroening · kroening · commit 7c32debc3f00 · 2022-06-30T16:23:08.000+01:00
diff --git a/src/solvers/smt2/smt2_conv.cpp b/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_array)
+  {
+    return "A" + type2id(to_array_type(type).element_type());
+  }
   else
   {
     UNREACHABLE;

Original file line number	Diff line number	Diff line change
`@@ -996,6 +996,10 @@ std::string smt2_convt::type2id(const typet &type) const`
`996`	`996`	`else`
`997`	`997`	`return "S" + std::to_string(boolbv_width(type));`
`998`	`998`	`}`
	`999`	`+ else if(type.id() == ID_array)`
	`1000`	`+ {`
	`1001`	`+ return "A" + type2id(to_array_type(type).element_type());`
	`1002`	`+ }`
`999`	`1003`	`else`
`1000`	`1004`	`{`
`1001`	`1005`	`UNREACHABLE;`