From e561387900b10744bb650258b8f9d9a4937e4f17 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sat, 6 Jun 2026 11:37:56 -0700
Subject: [PATCH] Handle `choice_k` in SMT pretty-printer switch to remove
 macOS `-Wswitch` warning (#9734)

`src/ast/ast_smt_pp.cpp` emitted a compiler warning on macOS because
`quantifier_kind::choice_k` was not handled in
`smt_printer::visit_quantifier`. This change makes the switch exhaustive
and preserves printer behavior for existing quantifier kinds.

- **Problem**
- `visit_quantifier` handled `forall_k`, `exists_k`, and `lambda_k`, but
omitted `choice_k`, triggering `-Wswitch`.

- **Change**
- Added an explicit `choice_k` branch in the quantifier-kind switch in
`/tmp/workspace/Z3Prover/z3/src/ast/ast_smt_pp.cpp`.
- The branch prints `choice` in SMT output, consistent with how other
quantifier headers are emitted.

- **Code snippet**
  ```cpp
  switch (q->get_kind()) {
  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;
  }
  ```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/ast/ast_smt_pp.cpp | 1 +
 1 file changed, 1 insertion(+)

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) {