mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
a6829ea9d0
commit
925867dc3e
|
@ -912,7 +912,7 @@ class smt2_printer {
|
|||
var_name = mk_smt2_quoted_symbol (*it);
|
||||
}
|
||||
else {
|
||||
var_name = it->str ();\
|
||||
var_name = it->str ();
|
||||
}
|
||||
buf.push_back(mk_seq1<format**,f2f>(m(), fs, fs+1, f2f(), var_name.c_str ()));
|
||||
}
|
||||
|
|
|
@ -34,6 +34,12 @@ bool is_smt2_quoted_symbol(char const * s) {
|
|||
if ('0' <= s[0] && s[0] <= '9')
|
||||
return true;
|
||||
unsigned len = static_cast<unsigned>(strlen(s));
|
||||
if (len > 2 && s[0] == '|' && s[len-1] == '|') {
|
||||
for (unsigned i = 1; i + 1 < len; i++)
|
||||
if (!is_smt2_simple_symbol_char(s[i]))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < len; i++)
|
||||
if (!is_smt2_simple_symbol_char(s[i]))
|
||||
return true;
|
||||
|
|
Loading…
Reference in a new issue