From d462ed3f0057a24fc1872a6a7a1e6ead34c970e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 May 2018 14:30:27 -0700 Subject: [PATCH] fix #1621 Signed-off-by: Nikolaj Bjorner --- src/util/smt2_util.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/util/smt2_util.cpp b/src/util/smt2_util.cpp index a218f0c27..365d8fe70 100644 --- a/src/util/smt2_util.cpp +++ b/src/util/smt2_util.cpp @@ -34,10 +34,14 @@ bool is_smt2_quoted_symbol(char const * s) { if ('0' <= s[0] && s[0] <= '9') return true; unsigned len = static_cast(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])) + if (len >= 2 && s[0] == '|' && s[len-1] == '|') { + for (unsigned i = 1; i + 1 < len; i++) { + if (s[i] == '\\' && i + 2 < len && (s[i+1] == '\\' || s[i+1] == '|')) { + i++; + } + else if (s[i] == '\\' || s[i] == '|') return true; + } return false; } for (unsigned i = 0; i < len; i++)