From a94d3a21ee6df7718a3b79cd0897a0ef6b66664b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Nov 2012 05:00:02 -0800
Subject: [PATCH] use same quotation mechanism as ast_smt2 parser

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_smt_pp.cpp | 25 ++-----------------------
 1 file changed, 2 insertions(+), 23 deletions(-)

diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index 944eb1e26..713727f05 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -29,6 +29,7 @@ Revision History:
 #include"vector.h"
 #include"for_each_ast.h"
 #include"decl_collector.h"
+#include"smt2_util.h"
 
 // ---------------------------------------
 // smt_renaming
@@ -67,32 +68,10 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
         return symbol(buffer.str().c_str());            
     }
     
-    buffer << "|";
-    if (*data == '|') {
-        while (*data) {
-            if (*data == '|') {
-                if (!data[1]) {
-                    break;
-                }
-                buffer << "\\";
-            }
-            buffer << *data;
-            ++data;
-        }                      
-    }
-    else {
-        while (*data) {
-            if (*data == '|') {
-                buffer << "\\";
-            }
-            buffer << *data;
-            ++data;
-        }
-    }
+    buffer << mk_smt2_quoted_symbol(s);
     if (k > 0) {
         buffer << k;
     }
-    buffer << "|";
     
     return symbol(buffer.str().c_str());
 }