diff options
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 6 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/printer/empty_symbol_name.smt2 | 8 |
3 files changed, 14 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 380004d02..66d36fe4c 100644 --- 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 261f8e19c..c39d96351 100644 --- 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 index 000000000..46652bc24 --- /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 (||)) |