diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index eb67083c2..72ac3a2a1 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -146,6 +146,7 @@ add_executable(test-z3
   theory_pb.cpp
   timeout.cpp
   tptp.cpp
+  ../shell/tptp_frontend.cpp
   total_order.cpp
   totalizer.cpp
   trigo.cpp
@@ -167,11 +168,9 @@ z3_add_gparams_register_modules_rule(${z3_test_deps})
 target_compile_definitions(test-z3 PRIVATE
   ${Z3_COMPONENT_CXX_DEFINES}
   Z3_TEST_SRC_DIR="${CMAKE_CURRENT_SOURCE_DIR}"
-  Z3_TEST_BIN_DIR="${PROJECT_BINARY_DIR}"
 )
 target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
 target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS})
 target_include_directories(test-z3 PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
 z3_append_linker_flag_list_to_target(test-z3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
 z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps})
-add_dependencies(test-z3 shell)
diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp
index 7d9daa85f..dc047c758 100644
--- a/src/test/tptp.cpp
+++ b/src/test/tptp.cpp
@@ -1,77 +1,29 @@
-#include <cstdio>
-#include <sstream>
 #include <string>
 #include <vector>
-#include <cctype>
 #include <iostream>
+#include <sstream>
 #include "util/debug.h"
-
-#ifdef _WINDOWS
-#define Z3_POPEN  _popen
-#define Z3_PCLOSE _pclose
-static char const* z3_bin_name = "z3.exe";
-#else
-#include <sys/wait.h>
-#define Z3_POPEN  popen
-#define Z3_PCLOSE pclose
-static char const* z3_bin_name = "z3";
-#endif
+#include "shell/tptp_frontend.h"
 
 struct tptp_case {
     char const* file;
     char const* expected_status;
 };
 
-constexpr unsigned command_output_buffer_size = 4096;
-
-static bool is_safe_file_name(char const* s) {
-    if (!s || !*s)
-        return false;
-    if (s[0] == '-' || s[0] == '.')
-        return false;
-    if (std::string(s).find('/') != std::string::npos || std::string(s).find('\\') != std::string::npos)
-        return false;
-    if (std::string(s).find("..") != std::string::npos)
-        return false;
-    while (*s) {
-        unsigned char c = static_cast<unsigned char>(*s);
-        if (!(std::isalnum(c) || c == '.' || c == '-' || c == '_'))
-            return false;
-        ++s;
-    }
-    return true;
-}
-
 static std::string run_tptp(char const* file) {
-    if (!is_safe_file_name(file)) {
-        std::cerr << "Unsafe TPTP test filename: " << file << "\n";
-        ENSURE(false);
-    }
-    std::ostringstream cmd;
-    cmd << "\"" << Z3_TEST_BIN_DIR << "/" << z3_bin_name << "\" -tptp "
-        << "\"" << Z3_TEST_SRC_DIR << "/tptp/" << file << "\" 2>&1";
-    FILE* pipe = Z3_POPEN(cmd.str().c_str(), "r");
-    if (!pipe) {
-        std::cerr << "Failed to execute command: " << cmd.str() << "\n";
-        ENSURE(false);
-    }
-    std::string out;
-    char buffer[command_output_buffer_size];
-    while (fgets(buffer, sizeof(buffer), pipe))
-        out += buffer;
-    int code = Z3_PCLOSE(pipe);
-#ifndef _WINDOWS
-    if (WIFEXITED(code))
-        code = WEXITSTATUS(code);
-#endif
-    if (code != 0) {
-        std::cerr << "TPTP command failed for file '" << file << "' with exit code " << code << "\n";
-        std::cerr << out << "\n";
-        ENSURE(false);
-    }
-    return out;
+    std::string path = std::string(Z3_TEST_SRC_DIR) + "/tptp/" + file;
+    std::streambuf* old_out = std::cout.rdbuf();
+    std::ostringstream out;
+    std::cout.rdbuf(out.rdbuf());
+    unsigned code = read_tptp(path.c_str());
+    std::cout.rdbuf(old_out);
+    ENSURE(code == 0);
+    return out.str();
 }
 
+bool g_display_statistics = false;
+bool g_display_model = false;
+
 void tst_tptp() {
     std::vector<tptp_case> cases = {
         {"agatha-butler.p", "% SZS status Theorem"},