From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 2 Dec 2019 22:21:05 +0000 (-0800)
Subject: [SMT2 Printer] Quote symbols starting with digit (#3517)
X-Git-Tag: cvc5-1.0.0~3809
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6bff71eab6102c1dd44698e75a0e1b0db72c2f65;p=cvc5.git

[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 1f45d8536..555908ea2 100644
--- 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 a098201b2..510316ae3 100644
--- 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
index 000000000..6a688a16f
--- /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))