Quote symbol when printing empty symbol name (#3025)

When printing an empty symbol name, which can appear in an SMT2 file as
`||`, we were printing the empty string instead of quoting the symbol.
This commit fixes the issue and adds a regression test.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 380004d02a50c41ababfd407eddb9f0b14131889..66d36fe4c5939385803641d79c87fb026dca6101 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -91,7 +91,11 @@ void Smt2Printer::toStream(
 
 static std::string maybeQuoteSymbol(const std::string& s) {
   // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted) symbols
-  if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") != string::npos) {
+  if (s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"
+                          "0123456789~!@$%^&*_-+=<>.?/")
+          != string::npos
+      || s.empty())
+  {
     // need to quote it
     stringstream ss;
     ss << '|' << s << '|';

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 261f8e19c0cd08b9cc5be5ff8e7cac6171431b09..c39d963519de2d9c2accf6185005ea95bc848538 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -585,6 +585,7 @@ set(regress_0_tests
   regress0/print_lambda.cvc
   regress0/printer/bv_consts_bin.smt2
   regress0/printer/bv_consts_dec.smt2
+  regress0/printer/empty_symbol_name.smt2
   regress0/printer/tuples_and_records.cvc
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2

diff --git a/test/regress/regress0/printer/empty_symbol_name.smt2 b/test/regress/regress0/printer/empty_symbol_name.smt2
new file mode 100644 (file)
index 0000000..46652bc
--- /dev/null
+++ b/test/regress/regress0/printer/empty_symbol_name.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+; EXPECT: ((|| (_ bv1 4)))
+(set-option :produce-models true)
+(set-logic QF_BV)
+(declare-const || (_ BitVec 4))
+(assert (= || #b0001))
+(check-sat)
+(get-value (||))