diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index bc277de42..cfe6698cf 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -1182,7 +1182,7 @@ class tptp_parser {
         if (let_consts.size() == 1) {
             replacer.insert(let_consts[0], value.get());
         } else {
-            throw parse_error("tuple $let destructuring is not supported");
+            throw parse_error("tuple $let destructuring is not supported; use single-variable $let bindings instead");
         }
         expr_ref result(m);
         replacer(body, result);
@@ -1257,7 +1257,7 @@ class tptp_parser {
 
         // Tuple/list in formula position: [t1, t2, ...] — return first element for simplicity
         if (accept(token_kind::lbrack)) {
-            throw parse_error("tuple/list formulas are not supported");
+            throw parse_error("tuple/list formulas are not supported in formula position; split them into separate formulas instead");
         }
 
         std::string n = parse_name();
@@ -1433,9 +1433,9 @@ class tptp_parser {
                     func_decl* f = mk_modal_op(mod_name);
                     return expr_ref(m.mk_app(f, sub.get()), m);
                 }
-                throw parse_error("tuple/list formulas are not supported");
+                throw parse_error("tuple/list formulas are not supported in formula position; split them into separate formulas instead");
             }
-            throw parse_error("tuple/list formulas are not supported");
+            throw parse_error("tuple/list formulas are not supported in formula position; split them into separate formulas instead");
         }
 
         // Diamond modality: <.>, <name>
diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp
index 42bd79d12..2bc216821 100644
--- a/src/test/tptp.cpp
+++ b/src/test/tptp.cpp
@@ -1,5 +1,7 @@
 #include <atomic>
+#include <cerrno>
 #include <cstdio>
+#include <cstring>
 #include <chrono>
 #include <filesystem>
 #include <fstream>
@@ -64,7 +66,7 @@ public:
     }
     ~scoped_temp_file() {
         if (!m_path.empty() && std::remove(m_path.c_str()) != 0)
-            std::cerr << "failed to remove temporary file: " << m_path << "\n";
+            std::cerr << "failed to remove temporary file '" << m_path << "': " << std::strerror(errno) << "\n";
     }
     std::string const& path() const { return m_path; }
 };