From 6bce1732483531e2ca65f34369bb449ba9e9c5fc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 12 Jun 2017 18:35:02 -0700
Subject: [PATCH] properly quote symbols #1061
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/cmd_context/basic_cmds.cpp | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 35e157af5..f6eea729f 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -149,7 +149,14 @@ ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {
first = false;
else
ctx.regular_stream() << " ";
- ctx.regular_stream() << "(" << escaped(name.str().c_str()) << " " << (ctx.m().is_true(val) ? "true" : "false") << ")";
+ ctx.regular_stream() << "(";
+ if (is_smt2_quoted_symbol(name)) {
+ ctx.regular_stream() << mk_smt2_quoted_symbol(name);
+ }
+ else {
+ ctx.regular_stream() << name;
+ }
+ ctx.regular_stream() << " " << (ctx.m().is_true(val) ? "true" : "false") << ")";
}
}
}