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

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