Upgrade to Z3 4.16.0 (#2578)

Author: parno

.github/workflows/get-z3.sh

@@ -22,7 +22,7 @@ Change directory to `source`: `cd source`
 ### On Windows: Get Z3 and set the `VERUS_Z3_PATH` environment variable
 
 Download the [Z3 binaries](https://github.com/Z3Prover/z3/releases).
-Make sure you get Z3 4.12.5.
+Make sure you get Z3 4.16.0.
 The Z3 `bin` folder contain the executable `z3.exe`.
 Set the `VERUS_Z3_PATH` environment variable to the path of the Z3 executable file.
 

BUILD.md

@@ -49,6 +49,11 @@ proof fn is_perfect_square_wlog(a: int, b: int, q: int) -> (sqrt: int)
     if a == 0 {
         assert(a * a == 0);
         assert(a * b == 0);
+        assert(b * b == q) by (nonlinear_arith)
+            requires
+                a == 0,
+                a * a + b * b == (a * b + 1) * q,
+        ;
         return b;
     } else {
         assert(b * b - (q * a) * b + (a * a - q) == 0) by {

examples/imo_1988_6.rs

@@ -117,10 +117,15 @@ pub(crate) fn smt_add_decl<'ctx>(context: &mut Context, decl: &Decl) {
 }
 
 impl SmtSolver {
-    pub fn reason_unknown_canceled_str(&self) -> &str {
+    /// The `(get-info :reason-unknown)` responses that mean "the solver hit its
+    /// resource/time budget".  These vary across Z3 versions.
+    pub fn reason_unknown_canceled_strs(&self) -> &'static [&'static str] {
         match self {
-            SmtSolver::Z3 => "(:reason-unknown \"canceled\")",
-            SmtSolver::Cvc5 => "(:reason-unknown resourceout)",
+            SmtSolver::Z3 => &[
+                "(:reason-unknown \"canceled\")",
+                "(:reason-unknown \"max. resource limit exceeded\")",
+            ],
+            SmtSolver::Cvc5 => &["(:reason-unknown resourceout)"],
         }
     }
 
@@ -290,7 +295,7 @@ pub(crate) fn smt_check_assertion<'ctx>(
 
             let mut reason = None;
             for line in smt_output {
-                if line == context.solver.reason_unknown_canceled_str() {
+                if context.solver.reason_unknown_canceled_strs().iter().any(|s| line == *s) {
                     assert!(reason == None);
                     reason = Some(SmtReasonUnknown::Canceled);
                 } else if line == "(:reason-unknown \"unknown\")" {

source/air/src/smt_verify.rs

@@ -50,7 +50,7 @@ error: function body check: Resource limit (rlimit) exceeded
 
 note: Analyzing prover log for (profile rerun) trigger_loops::trigger_forever2 ...
 
-Z3 4.12.5
+Z3 4.16.0
 note: Log analysis complete for (profile rerun) trigger_loops::trigger_forever2
 
 note: Profile statistics for trigger_loops::trigger_forever2

source/docs/guide/src/profiling.md

@@ -1351,6 +1351,12 @@ test_verify_one_file_with_options! {
                 if result as u64 * result as u64 > n as u64 {
                     break;
                 }
+                assert(n != 1 ==> 1 <= result < n) by (nonlinear_arith)
+                    requires
+                        1 <= result,
+                        result as u64 * result as u64 <= n as u64,
+                        1 <= n,
+                { }
             }
             result - 1
         }

source/rust_verify_test/tests/loops.rs

@@ -339,6 +339,7 @@ test_verify_one_file! {
             let x = (-128i8) / (-1i8); // FAILS
         }
 
+        #[verifier::spinoff_prover]
         fn test_signed_mod() {
             let x = 53i8 % 10i8;
             assert(x == 3);

source/rust_verify_test/tests/operators.rs

@@ -1,4 +1,4 @@
-$z3_version = "4.12.5"
+$z3_version = "4.16.0"
 $filename = "z3-$z3_version-x64-win"
 
 $download_url = "https://github.com/Z3Prover/z3/releases/download/z3-$z3_version/$filename.zip"

source/tools/get-z3.ps1

@@ -1,21 +1,25 @@
 #! /bin/bash -eu
 
-z3_version="4.12.5"
+z3_version="4.16.0"
 
+# The OS/libc suffix in each release artifact's name is specific to the Z3
+# version (it tracks the platform Z3's CI built that release on), so these
+# strings must be revisited on every Z3 upgrade -- they cannot be derived from
+# $z3_version alone. See https://github.com/Z3Prover/z3/releases.
 if [ `uname` == "Darwin" ]; then
     if [[ $(uname -m) == 'arm64' ]]; then
-        filename="z3-$z3_version-arm64-osx-11.0"
+        filename="z3-$z3_version-arm64-osx-15.7.3"
     elif [[ $(uname -m) == 'x86_64' ]]; then
-        filename="z3-$z3_version-x64-osx-11.7.10"
+        filename="z3-$z3_version-x64-osx-15.7.3"
     else
         echo "Unsupported architecture $(uname -m)"
         exit -1
     fi
 elif [ `uname` == "Linux" ]; then
     if [[ $(uname -m) == 'aarch64' ]]; then
-        filename="z3-$z3_version-arm64-glibc-2.35"
+        filename="z3-$z3_version-arm64-glibc-2.38"
     elif [[ $(uname -m) == 'x86_64' ]]; then
-        filename="z3-$z3_version-x64-glibc-2.31"
+        filename="z3-$z3_version-x64-glibc-2.39"
     else
         echo "Unsupported architecture $(uname -m)"
         exit -1

source/tools/get-z3.sh

@@ -17,6 +17,7 @@ use super::super::prelude::*;
 
 verus! {
 
+#[verifier::inline]
 pub open spec fn rust_div(a: int, b: int) -> int
     recommends
         b != 0,
@@ -30,6 +31,7 @@ pub open spec fn rust_div(a: int, b: int) -> int
     }
 }
 
+#[verifier::inline]
 pub open spec fn rust_rem(a: int, b: int) -> int
     recommends
         b != 0,
@@ -745,6 +747,7 @@ pub broadcast proof fn lemma_div_multiples_vanish_quotient(x: int, a: int, d: in
 
 /// Proof that, since `a % d == 0` and `0 <= r < d`, we can conclude
 /// `a == d * (a + r) / d`.
+#[verifier::spinoff_prover]
 pub broadcast proof fn lemma_round_down(a: int, r: int, d: int)
     requires
         0 < d,