From 594f31319dc8a2ddd7656e13d94339421b016c41 Mon Sep 17 00:00:00 2001
From: Mate Kovacs <mkovaxx@gmail.com>
Date: Tue, 26 May 2026 22:34:12 +0900
Subject: [PATCH] use a fresh temp dir to isolate test runs

---
 source/rust_verify_test/tests/cargo.rs      | 20 +++++++---------
 source/rust_verify_test/tests/common/mod.rs | 26 +++++++++++++++++++--
 2 files changed, 32 insertions(+), 14 deletions(-)

diff --git a/source/rust_verify_test/tests/cargo.rs b/source/rust_verify_test/tests/cargo.rs
index b0cb5275ec..f01972a080 100644
--- a/source/rust_verify_test/tests/cargo.rs
+++ b/source/rust_verify_test/tests/cargo.rs
@@ -59,21 +59,19 @@ fn run_cargo_verus_for_dir(dir: &str) {
         extra_verus_args.extend(args.split(" "));
     }
 
-    // Don't reuse any artifacts from previous runs
-    let args = vec!["clean"];
-    let run = run_cargo(&args, &test_dir.as_path());
-    assert!(run.status.success());
+    // Use a temp dir for the target dir to isolate each test run
+    let target_dir = tempdir().expect("Failed to create temporary target directory");
 
     let mut args = vec!["verify"];
     args.push("--");
     args.extend(&extra_verus_args);
-    let run = run_cargo_verus(&args, &test_dir.as_path());
+    let run = run_cargo_verus_with_target(&args, &test_dir, target_dir.path());
     assert!(run.status.success());
 
     let mut args = vec!["build"];
     args.push("--");
     args.extend(&extra_verus_args);
-    let run = run_cargo_verus(&args, &test_dir.as_path());
+    let run = run_cargo_verus_with_target(&args, &test_dir, target_dir.path());
     assert!(run.status.success());
 }
 
@@ -91,17 +89,15 @@ fn run_vanilla_cargo_for_dir(dir: &str) {
         return;
     }
 
-    // Don't reuse any artifacts from previous runs
-    let args = vec!["clean"];
-    let run = run_cargo(&args, &test_dir.as_path());
-    assert!(run.status.success());
+    // Use a temp dir for the target dir to isolate each test run
+    let target_dir = tempdir().expect("Failed to create temporary target directory");
 
     let args = vec!["check"];
-    let run = run_cargo(&args, &test_dir.as_path());
+    let run = run_cargo_with_target(&args, &test_dir, target_dir.path());
     assert!(run.status.success());
 
     let args = vec!["build"];
-    let run = run_cargo(&args, &test_dir.as_path());
+    let run = run_cargo_with_target(&args, &test_dir, target_dir.path());
     assert!(run.status.success());
 }
 
diff --git a/source/rust_verify_test/tests/common/mod.rs b/source/rust_verify_test/tests/common/mod.rs
index d2ef7d979b..081a7a932b 100644
--- a/source/rust_verify_test/tests/common/mod.rs
+++ b/source/rust_verify_test/tests/common/mod.rs
@@ -444,6 +444,14 @@ pub fn run_verus(
 }
 
 pub fn run_cargo_verus(args: &[&str], dir: &std::path::Path) -> std::process::Output {
+    run_cargo_verus_with_target(args, dir, &dir.join("target"))
+}
+
+pub fn run_cargo_verus_with_target(
+    args: &[&str],
+    dir: &std::path::Path,
+    target_dir: &std::path::Path,
+) -> std::process::Output {
     if std::env::var("VERUS_IN_VARGO").is_err() {
         panic!("not running in vargo, read the README for instructions");
     }
@@ -471,6 +479,9 @@ pub fn run_cargo_verus(args: &[&str], dir: &std::path::Path) -> std::process::Ou
 
     let mut child = std::process::Command::new(bin);
     child.current_dir(dir);
+    child.env("CARGO_TARGET_DIR", target_dir);
+    child.env("CARGO_BUILD_TARGET_DIR", target_dir);
+    child.env("CARGO_BUILD_BUILD_DIR", target_dir);
 
     let z3 = std::env::var("VERUS_Z3_PATH")
         .map(|p| {
@@ -489,7 +500,7 @@ pub fn run_cargo_verus(args: &[&str], dir: &std::path::Path) -> std::process::Ou
     child.env("VERUS_Z3_PATH", z3);
 
     let child = child
-        .args(&args[..])
+        .args(args)
         .stdout(std::process::Stdio::piped())
         .stderr(std::process::Stdio::piped())
         .spawn()
@@ -504,6 +515,14 @@ pub fn run_cargo_verus(args: &[&str], dir: &std::path::Path) -> std::process::Ou
 
 // Assumes normal `cargo` is in the caller's path
 pub fn run_cargo(args: &[&str], dir: &std::path::Path) -> std::process::Output {
+    run_cargo_with_target(args, dir, &dir.join("target"))
+}
+
+pub fn run_cargo_with_target(
+    args: &[&str],
+    dir: &std::path::Path,
+    target_dir: &std::path::Path,
+) -> std::process::Output {
     // if std::env::var("VERUS_IN_VARGO").is_err() {
     //     panic!("not running in vargo, read the README for instructions");
     // }
@@ -513,9 +532,12 @@ pub fn run_cargo(args: &[&str], dir: &std::path::Path) -> std::process::Output {
     // Remove Verus-specific RUSTFLAGS that are set by vargo, as they cause
     // verus_builtin and vstd to require unstable features not available on stable Rust
     child.env_remove("RUSTFLAGS");
+    child.env("CARGO_TARGET_DIR", target_dir);
+    child.env("CARGO_BUILD_TARGET_DIR", target_dir);
+    child.env("CARGO_BUILD_BUILD_DIR", target_dir);
 
     let child = child
-        .args(&args[..])
+        .args(args)
         .stdout(std::process::Stdio::piped())
         .stderr(std::process::Stdio::piped())
         .spawn()