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") << ")"; } } }