diff --git a/src/test/api.cpp b/src/test/api.cpp
index 560dd1121..1cd21e7c7 100644
--- a/src/test/api.cpp
+++ b/src/test/api.cpp
@@ -11,6 +11,8 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/trace.h"
 #include <map>
 #include "util/trace.h"
+#include <thread>
+#include <vector>
 
 void test_apps() {
     Z3_config cfg = Z3_mk_config();
@@ -104,11 +106,73 @@ static void test_mk_distinct() {
     VERIFY(!d);
     Z3_del_config(cfg);
     Z3_del_context(ctx);    
+}
+
+// Test for race condition in Z3_solver_translate when used in multiple threads
+// Reproduces issue: https://github.com/prove-rs/z3.rs/issues/465
+static void test_solver_translate_threading() {
+    auto thread_fn = []() {
+        Z3_config cfg = Z3_mk_config();
+        Z3_context ctx1 = Z3_mk_context(cfg);
+        Z3_del_config(cfg);
+        
+        Z3_solver s = Z3_mk_solver(ctx1);
+        Z3_solver_inc_ref(ctx1, s);
+        
+        // Create variables
+        Z3_sort int_sort = Z3_mk_int_sort(ctx1);
+        Z3_symbol x_sym = Z3_mk_string_symbol(ctx1, "x");
+        Z3_symbol y_sym = Z3_mk_string_symbol(ctx1, "y");
+        Z3_ast x = Z3_mk_const(ctx1, x_sym, int_sort);
+        Z3_ast y = Z3_mk_const(ctx1, y_sym, int_sort);
+        
+        // Add constraints: y < 2
+        Z3_ast two = Z3_mk_int(ctx1, 2, int_sort);
+        Z3_ast y_lt_2 = Z3_mk_lt(ctx1, y, two);
+        Z3_solver_assert(ctx1, s, y_lt_2);
+        
+        // Add constraints: x * y = -2
+        Z3_ast neg_two = Z3_mk_int(ctx1, -2, int_sort);
+        Z3_ast args[] = {x, y};
+        Z3_ast mul = Z3_mk_mul(ctx1, 2, args);
+        Z3_ast eq = Z3_mk_eq(ctx1, mul, neg_two);
+        Z3_solver_assert(ctx1, s, eq);
+        
+        // Create new context and translate
+        Z3_config cfg2 = Z3_mk_config();
+        Z3_context ctx2 = Z3_mk_context(cfg2);
+        Z3_del_config(cfg2);
+        
+        Z3_solver s2 = Z3_solver_translate(ctx1, s, ctx2);
+        Z3_solver_inc_ref(ctx2, s2);
+        
+        // Check satisfiability - should be SAT
+        Z3_lbool result = Z3_solver_check(ctx2, s2);
+        ENSURE(result == Z3_L_TRUE);
+        
+        // Cleanup
+        Z3_solver_dec_ref(ctx2, s2);
+        Z3_del_context(ctx2);
+        Z3_solver_dec_ref(ctx1, s);
+        Z3_del_context(ctx1);
+    };
     
+    std::vector<std::thread> threads;
+    
+    // Create multiple threads (more than typical CPU cores to trigger potential race)
+    for (int i = 0; i < 20; ++i) {
+        threads.emplace_back(thread_fn);
+    }
+    
+    // Join all threads
+    for (auto& t : threads) {
+        t.join();
+    }
 }
 
 void tst_api() {
     test_apps();
     test_bvneg();
     test_mk_distinct();
+    test_solver_translate_threading();
 }
diff --git a/test_translate_race b/test_translate_race
deleted file mode 100755
index 534f97ae8..000000000
Binary files a/test_translate_race and /dev/null differ
diff --git a/test_translate_race.cpp b/test_translate_race.cpp
deleted file mode 100644
index b96db81b1..000000000
--- a/test_translate_race.cpp
+++ /dev/null
@@ -1,87 +0,0 @@
-// Test to reproduce the race condition in Z3_solver_translate
-#include <iostream>
-#include <thread>
-#include <vector>
-#include "z3.h"
-
-void test_thread() {
-    Z3_config cfg = Z3_mk_config();
-    Z3_context ctx1 = Z3_mk_context(cfg);
-    Z3_del_config(cfg);
-    
-    Z3_solver s = Z3_mk_solver(ctx1);
-    Z3_solver_inc_ref(ctx1, s);
-    
-    // Create variables
-    Z3_sort int_sort = Z3_mk_int_sort(ctx1);
-    Z3_symbol x_sym = Z3_mk_string_symbol(ctx1, "x");
-    Z3_symbol y_sym = Z3_mk_string_symbol(ctx1, "y");
-    Z3_ast x = Z3_mk_const(ctx1, x_sym, int_sort);
-    Z3_ast y = Z3_mk_const(ctx1, y_sym, int_sort);
-    Z3_inc_ref(ctx1, x);
-    Z3_inc_ref(ctx1, y);
-    
-    // Add constraints: y < 2
-    Z3_ast two = Z3_mk_int(ctx1, 2, int_sort);
-    Z3_inc_ref(ctx1, two);
-    Z3_ast y_lt_2 = Z3_mk_lt(ctx1, y, two);
-    Z3_inc_ref(ctx1, y_lt_2);
-    Z3_solver_assert(ctx1, s, y_lt_2);
-    
-    // Add constraints: x * y = -2
-    Z3_ast neg_two = Z3_mk_int(ctx1, -2, int_sort);
-    Z3_inc_ref(ctx1, neg_two);
-    Z3_ast args[] = {x, y};
-    Z3_ast mul = Z3_mk_mul(ctx1, 2, args);
-    Z3_inc_ref(ctx1, mul);
-    Z3_ast eq = Z3_mk_eq(ctx1, mul, neg_two);
-    Z3_inc_ref(ctx1, eq);
-    Z3_solver_assert(ctx1, s, eq);
-    
-    // Create new context and translate
-    Z3_config cfg2 = Z3_mk_config();
-    Z3_context ctx2 = Z3_mk_context(cfg2);
-    Z3_del_config(cfg2);
-    
-    Z3_solver s2 = Z3_solver_translate(ctx1, s, ctx2);
-    Z3_solver_inc_ref(ctx2, s2);
-    
-    // Check satisfiability
-    Z3_lbool result = Z3_solver_check(ctx2, s2);
-    
-    if (result != Z3_L_TRUE) {
-        std::cerr << "Thread " << std::this_thread::get_id() 
-                  << " got unexpected result: " << result 
-                  << " (expected SAT)" << std::endl;
-    }
-    
-    // Cleanup
-    Z3_solver_dec_ref(ctx2, s2);
-    Z3_del_context(ctx2);
-    Z3_dec_ref(ctx1, eq);
-    Z3_dec_ref(ctx1, mul);
-    Z3_dec_ref(ctx1, neg_two);
-    Z3_dec_ref(ctx1, y_lt_2);
-    Z3_dec_ref(ctx1, two);
-    Z3_dec_ref(ctx1, y);
-    Z3_dec_ref(ctx1, x);
-    Z3_solver_dec_ref(ctx1, s);
-    Z3_del_context(ctx1);
-}
-
-int main() {
-    std::vector<std::thread> threads;
-    
-    // Create multiple threads (more than CPU cores to trigger the issue)
-    for (int i = 0; i < 20; ++i) {
-        threads.emplace_back(test_thread);
-    }
-    
-    // Join all threads
-    for (auto& t : threads) {
-        t.join();
-    }
-    
-    std::cout << "Test completed" << std::endl;
-    return 0;
-}