From 5ebf5a0d9f8c8d22fd6ff0593f1d5318e94043e9 Mon Sep 17 00:00:00 2001
From: Can Cebeci <can.cebeci99@gmail.com>
Date: Thu, 4 Jun 2026 15:48:27 -0700
Subject: [PATCH] Fix quoting in low-level pretty printer (#9716)

Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
---
 src/ast/ast_ll_pp.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
index 301d23b05..10a08f2d5 100644
--- a/src/ast/ast_ll_pp.cpp
+++ b/src/ast/ast_ll_pp.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "ast/for_each_ast.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/ast_smt2_pp.h"
 
 // #define AST_LL_PP_SHOW_FAMILY_NAME
 
@@ -44,7 +45,7 @@ class ll_printer {
     }
 
     void display_name(func_decl * decl) {
-        m_out << decl->get_name();
+        m_out << ensure_quote(decl->get_name());
     }
 
     bool process_numeral(expr * n) {