From c4cb5bbc15f073c891adc435878a1120113a9b45 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 14 Jul 2026 11:16:47 -0700
Subject: [PATCH] update release.yml and tptp_frontend

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .github/workflows/release.yml     | 10 ++++++++++
 src/cmd_context/tptp_frontend.cpp | 12 ++++--------
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 5e1d3eeefa..84614da7eb 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -917,6 +917,16 @@ jobs:
         with:
           name: PythonPackage
           path: dist
+
+      - name: Rewrite macOS wheel tags unsupported by test.PyPI
+        run: |
+          # TestPyPI rejects current macOS wheel tags such as macosx_13_3_*.
+          # Rewrite only the unsupported 13_3 tag to 13 for upload validation.
+          for whl in dist/*-macosx_13_3_*.whl; do
+            [ -e "$whl" ] || continue
+            mv "$whl" "${whl/macosx_13_3_/macosx_13_0_}"
+          done
+          ls -l dist      
       
       - name: Publish to PyPI
         uses: pypa/gh-action-pypi-publish@release/v1
diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index 65368bfc40..966e026cab 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -1508,7 +1508,7 @@ class tptp_parser {
     // For function-style definitions, wraps value in lambdas over the parameter variables.
     std::pair<std::string, expr_ref> parse_single_let_defn() {
         std::string name = parse_name();
-        std::vector<app*> param_vars;
+        ptr_vector<app> param_vars;
         std::unordered_map<std::string, app*> param_scope;
         if (accept(token_kind::lparen)) {
             if (!accept(token_kind::rparen)) {
@@ -2947,13 +2947,9 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) {
                 dout << "; Auto-generated from TPTP input: "
                      << (current_file ? current_file : "?") << "\n";
                 dout << "(set-logic ALL)\n";
-                decl_collector decls(m);
-                for (expr* a : ctx.assertions())
-                    decls.visit(a);
-                for (sort* s : decls.get_sorts())
-                    if (m.is_uninterp(s) && s->get_num_parameters() == 0)
-                        dout << "(declare-sort " << s->get_name() << " 0)\n";
-                ctx.display_smt2_benchmark(dout, ctx.assertions().size(), ctx.assertions().data());
+                dout << "(set-param :pi.avoid_skolems false)\n";
+                ctx.get_solver()->display(dout);
+                dout << "(check-sat)\n";
             }
         }