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_terms.cpp

@@ -39,7 +39,7 @@ TEST_CASE("smt_identifier_termt construction", "[core][smt2_incremental]")
   cbmc_invariants_should_throwt invariants_throw;
   CHECK_NOTHROW(smt_identifier_termt{"foo bar", smt_bool_sortt{}});
   CHECK_THROWS(smt_identifier_termt{"|foo bar|", smt_bool_sortt{}});
-  CHECK_THROWS(smt_identifier_termt{"foo\\ bar", smt_bool_sortt{}});
+  CHECK_NOTHROW(smt_identifier_termt{"foo\\ bar", smt_bool_sortt{}});
 }
 
 TEST_CASE("smt_identifier_termt getters.", "[core][smt2_incremental]")

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]")