Skip to content

Commit ddedba8

Browse files
committed
Do not quote identifiers matching definition of simple_symbol from SMT-lib spec
1 parent 4987df3 commit ddedba8

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,13 +13,17 @@
1313

1414
#include <functional>
1515
#include <iostream>
16+
#include <regex>
1617
#include <sstream>
1718
#include <stack>
1819
#include <string>
1920

2021
static std::string escape_identifier(const irep_idt &identifier)
2122
{
22-
return std::string{"|"} + smt2_convt::convert_identifier(identifier) + "|";
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 + "|";
2327
}
2428

2529
class smt_index_output_visitort : public smt_index_const_downcast_visitort

0 commit comments

Comments
 (0)