Fix guard identifier processing

The identifier for guards includes the `\` character. Therefore this
commit is needed for allowing smt identifiers to be constructed
including this character and converted to string.

Author: thomasspriggs

src/solvers/smt2_incremental/smt_terms.cpp

@@ -50,7 +50,7 @@ bool smt_bool_literal_termt::value() const
 
 static bool is_valid_smt_identifier(irep_idt identifier)
 {
-  static const std::regex valid{R"(^[^\|\\]*$)"};
+  static const std::regex valid{R"(^[^\|]*$)"};
   return std::regex_match(id2string(identifier), valid);
 }
 
@@ -59,7 +59,7 @@ smt_identifier_termt::smt_identifier_termt(irep_idt identifier, smt_sortt sort)
 {
   INVARIANT(
     is_valid_smt_identifier(identifier),
-    R"(Identifiers may not contain | or \ characters.)");
+    R"(Identifiers may not contain | characters.)");
   set(ID_identifier, identifier);
 }
 

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -32,6 +32,18 @@ TEST_CASE(
   CHECK(smt_to_smt2_string(smt_bool_literal_termt{false}) == "false");
 }
 
+TEST_CASE(
+  "Test smt_identifier_termt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(
+    smt_to_smt2_string(smt_identifier_termt{"abc", smt_bool_sortt{}}) ==
+    "|abc|");
+  CHECK(
+    smt_to_smt2_string(smt_identifier_termt{"\\", smt_bool_sortt{}}) ==
+    "|&92;|");
+}
+
 TEST_CASE(
   "Test smt_function_application_termt to string conversion",
   "[core][smt2_incremental]")