diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index aeaebc6bf..ade12de62 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -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 ()));
         }
diff --git a/src/util/smt2_util.cpp b/src/util/smt2_util.cpp
index 8358c67ac..a218f0c27 100644
--- a/src/util/smt2_util.cpp
+++ b/src/util/smt2_util.cpp
@@ -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;