[SMT2 Printer] Quote symbols starting with digit (#3517)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1f45d8536f4e17d5fc0d90fb3d476f6dbeef4aaa..555908ea2878b42d91ecf49d082f27bbe29b14ce 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -95,7 +95,7 @@ static std::string maybeQuoteSymbol(const std::string& s) {
   if (s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"
                           "0123456789~!@$%^&*_-+=<>.?/")
           != string::npos
-      || s.empty())
+      || s.empty() || (s[0] >= '0' && s[0] <= '9'))
   {
     // need to quote it
     stringstream ss;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a098201b26bcd2bdcc901de7d83f5b6d5beaf3ea..510316ae3e24d3e0a370af1bad73d5c3672819e1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -612,6 +612,7 @@ set(regress_0_tests
   regress0/printer/bv_consts_dec.smt2
   regress0/printer/empty_symbol_name.smt2
   regress0/printer/let_shadowing.smt2
+  regress0/printer/symbol_starting_w_digit.smt2
   regress0/printer/tuples_and_records.cvc
   regress0/proof_no_support.smt2
   regress0/push-pop/boolean/fuzz_12.smt2

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