diff --git a/Cargo.lock b/Cargo.lock
index 77aff5b000..cde6734589 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2791,9 +2791,9 @@ dependencies = [
 
 [[package]]
 name = "z3"
-version = "0.6.0"
+version = "0.7.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f0354c65dfe00e08c4ab30581732906874f97156f424bfb390cf0cca2cb6ac29"
+checksum = "dbb8ef9d11f50b64327c8a5906b53d3f7f792cb0e849909d476ac0aa16117d61"
 dependencies = [
  "lazy_static",
  "log",
@@ -2802,9 +2802,9 @@ dependencies = [
 
 [[package]]
 name = "z3-sys"
-version = "0.6.2"
+version = "0.6.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e1863cafae8eb86dd7d69c9218421b288594e8836346e93d4f36ade427195a21"
+checksum = "afa18ba5fbd4933e41ffb440c3fd91f91fe9cdb7310cce3ddfb6648563811de0"
 dependencies = [
  "cmake",
 ]
diff --git a/cranelift/peepmatic/Cargo.toml b/cranelift/peepmatic/Cargo.toml
index 53e958973b..c8cab33e60 100644
--- a/cranelift/peepmatic/Cargo.toml
+++ b/cranelift/peepmatic/Cargo.toml
@@ -16,7 +16,7 @@ peepmatic-runtime = { version = "0.67.0", path = "crates/runtime", features = ["
 peepmatic-traits = { version = "0.67.0", path = "crates/traits" }
 serde = { version = "1.0.105", features = ["derive"] }
 wast = "25.0.0"
-z3 = { version = "0.6.0", features = ["static-link-z3"] }
+z3 = { version = "0.7.0", features = ["static-link-z3"] }
 
 [dev-dependencies]
 peepmatic-test-operator = { version = "0.67.0", path = "crates/test-operator" }
diff --git a/cranelift/peepmatic/src/verify.rs b/cranelift/peepmatic/src/verify.rs
index 978a0cf1ee..26bf22f9df 100644
--- a/cranelift/peepmatic/src/verify.rs
+++ b/cranelift/peepmatic/src/verify.rs
@@ -237,13 +237,13 @@ struct TypingContext<'a, TOperator> {
 
 impl<'a, TOperator> TypingContext<'a, TOperator> {
     fn new(z3: &'a z3::Context) -> Self {
-        let type_kind_sort = z3::DatatypeBuilder::new(z3)
-            .variant("int", &[])
-            .variant("bool", &[])
-            .variant("cpu_flags", &[])
-            .variant("cc", &[])
-            .variant("void", &[])
-            .finish("TypeKind");
+        let type_kind_sort = z3::DatatypeBuilder::new(z3, "TypeKind")
+            .variant("int", vec![])
+            .variant("bool", vec![])
+            .variant("cpu_flags", vec![])
+            .variant("cc", vec![])
+            .variant("void", vec![])
+            .finish();
         TypingContext {
             z3,
             solver: z3::Solver::new(z3),
@@ -576,7 +576,7 @@ impl<'a, TOperator> TypingContext<'a, TOperator> {
         // Check if there is more than one satisfying assignment to
         // `ty_var`'s width variable. If so, then it must be polymorphic. If
         // not, then it must have a fixed value.
-        let model = self.solver.get_model();
+        let model = self.solver.get_model().unwrap();
         let width_var = model.eval(&ty_var.width).unwrap();
         let bit_width: u8 = width_var.as_u64().unwrap().try_into().unwrap();