diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index db52a583f..852e81cf1 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -507,6 +507,7 @@ class smt_printer {
         case forall_k: m_out << "forall "; break;
         case exists_k: m_out << "exists "; break;
         case lambda_k: m_out << "lambda "; break;
+        case choice_k: m_out << "choice "; break;
         }
         m_out << "(";
         for (unsigned i = 0; i < q->get_num_decls(); ++i) {