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.
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 << '|';
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
--- /dev/null
+; EXPECT: sat
+; EXPECT: ((|| (_ bv1 4)))
+(set-option :produce-models true)
+(set-logic QF_BV)
+(declare-const || (_ BitVec 4))
+(assert (= || #b0001))
+(check-sat)
+(get-value (||))