From b72d64ff08885f37d0d1f170d1c945fc1e3684c6 Mon Sep 17 00:00:00 2001 From: "Chris Hawblitzel (Microsoft)" Date: Wed, 26 Jul 2023 21:10:20 -0700 Subject: [PATCH] Change vargo warning to handle preexisting VERUS_Z3_PATH (#708) --- tools/vargo/src/main.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/tools/vargo/src/main.rs b/tools/vargo/src/main.rs index c931f08321..45fca1d64d 100644 --- a/tools/vargo/src/main.rs +++ b/tools/vargo/src/main.rs @@ -231,10 +231,15 @@ fn run() -> Result<(), String> { std::env::set_var("VARGO_TOOLCHAIN", toolchain); } - let z3_path = std::path::Path::new(Z3_FILE_NAME); + let z3_file_name = if vargo_nest == 0 && std::env::var("VERUS_Z3_PATH").is_ok() { + std::env::var("VERUS_Z3_PATH").unwrap() + } else { + Z3_FILE_NAME.to_string() + }; + let z3_path = std::path::Path::new(&z3_file_name); if !z3_path.is_file() && vargo_nest == 0 { - warn(format!("{Z3_FILE_NAME} not found -- this is likely to cause errors or a broken build\nrun `tools/get-z3.(sh|ps1)` first").as_str()); + warn(format!("{z3_file_name} not found -- this is likely to cause errors or a broken build\nrun `tools/get-z3.(sh|ps1)` first").as_str()); } if std::env::var("VERUS_Z3_PATH").is_err() && z3_path.is_file() { std::env::set_var("VERUS_Z3_PATH", z3_path);