From aef3de5fca6fd7ae07bb9223eaf71783ce257909 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 12 Apr 2018 15:05:35 +0800
Subject: [PATCH] escape ascii above 127, issue #1571

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index c9dbc78f8..b592b719a 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -213,6 +213,9 @@ std::string zstring::encode() const {
         else if (ch == '\\') {
             strm << "\\\\";
         }
+        else if (ch >= 128) {
+            strm << "\\x" << std::hex << (unsigned)ch << std::dec; 
+        }
         else {
             strm << (char)(ch);
         }