bugfix: fix 'vargo build --no-solver-version-check', fixes #1313

verus-lang · Oct 22, 2024 · de60bcd · de60bcd
1 parent 8a20b87
commit de60bcd
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 1 deletion.
diff --git a/source/tools/get-z3.sh b/source/tools/get-z3.sh
@@ -1,6 +1,6 @@
 #! /bin/bash -eu
 
-z3_version="4.12.5"
+z3_version="4.13.0"
 
 if [ `uname` == "Darwin" ]; then
     if [[ $(uname -m) == 'arm64' ]]; then

diff --git a/source/vstd_build/src/main.rs b/source/vstd_build/src/main.rs
@@ -32,6 +32,7 @@ fn main() {
     let mut verbose = false;
     let mut trace = false;
     let mut log_all = false;
+    let mut no_solver_version_check = false;
     for arg in args {
         if arg == "--release" {
             release = true;
@@ -47,6 +48,8 @@ fn main() {
             trace = true;
         } else if arg == "--log-all" {
             log_all = true;
+        } else if arg == "--no-solver-version-check" {
+            no_solver_version_check = true;
         } else {
             panic!("unexpected argument: {:}", arg)
         }
@@ -110,6 +113,10 @@ fn main() {
     if log_all {
         child_args.push("--log-all".to_string());
     }
+    if no_solver_version_check {
+        child_args.push("-V".to_string());
+        child_args.push("no-solver-version-check".to_string());
+    }
     if release {
         child_args.push("-C".to_string());
         child_args.push("opt-level=3".to_string());

diff --git a/tools/vargo/src/main.rs b/tools/vargo/src/main.rs
@@ -1306,6 +1306,9 @@ set -x
                         if verbose {
                             vstd_build = vstd_build.arg("--verbose");
                         }
+                        if no_solver_version_check {
+                            vstd_build = vstd_build.arg("--no-solver-version-check");
+                        }
                         log_command(&vstd_build, verbose);
                         vstd_build
                             .status()