Skip to content

Commit 8112492

Browse files
committed
Change regex_match to match against the identifier rather than the converted string
1 parent ddedba8 commit 8112492

File tree

1 file changed

+8
-4
lines changed

1 file changed

+8
-4
lines changed

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,14 @@
2020

2121
static std::string escape_identifier(const irep_idt &identifier)
2222
{
23-
const std::string &quoted_identifier = smt2_convt::convert_identifier(identifier);
24-
if (std::regex_match(quoted_identifier, std::regex("(\\w+)|\\+-/\\*=%?!\\.\\$_~&\\^<>@")))
25-
return quoted_identifier;
26-
return std::string{"|"} + quoted_identifier + "|";
23+
// This matches the definition of a `simple_symbol` according to the SMTLIB
24+
// specification, version 2.6.
25+
const std::regex simple_symbol_regex(
26+
"[a-zA-Z\\+-\\/\\*=%?!\\.\\$_~&\\^<>@][\\w\\+-\\/\\*=%?!\\.\\$_~&\\^<>@]*");
27+
if(std::regex_match(id2string(identifier), simple_symbol_regex))
28+
return id2string(identifier);
29+
30+
return std::string{"|"} + smt2_convt::convert_identifier(identifier) + "|";
2731
}
2832

2933
class smt_index_output_visitort : public smt_index_const_downcast_visitort

0 commit comments

Comments
 (0)