From 02e63faf8125ce7e8f64f67a26aaa45538205636 Mon Sep 17 00:00:00 2001
From: Alexa VanHattum <amv94@cornell.edu>
Date: Wed, 14 Feb 2024 15:48:53 -0500
Subject: [PATCH] Add max width

---
 cranelift/isle/veri/veri_engine/src/lib.rs    |  3 +++
 cranelift/isle/veri/veri_engine/src/solver.rs | 12 ++++++------
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/cranelift/isle/veri/veri_engine/src/lib.rs b/cranelift/isle/veri/veri_engine/src/lib.rs
index e183bd5efbf5..dfc315b9ee36 100644
--- a/cranelift/isle/veri/veri_engine/src/lib.rs
+++ b/cranelift/isle/veri/veri_engine/src/lib.rs
@@ -15,6 +15,9 @@ pub mod verify;
 
 pub const REG_WIDTH: usize = 64;
 
+// Use a distinct with as the maximum width any value should have within type inference
+pub const MAX_WIDTH: usize = 4*REG_WIDTH;
+
 pub const FLAGS_WIDTH: usize = 4;
 
 pub const WIDTHS: [usize; 4] = [8, 16, 32, 64];
diff --git a/cranelift/isle/veri/veri_engine/src/solver.rs b/cranelift/isle/veri/veri_engine/src/solver.rs
index 962a945d0b07..adc904bcec87 100644
--- a/cranelift/isle/veri/veri_engine/src/solver.rs
+++ b/cranelift/isle/veri/veri_engine/src/solver.rs
@@ -23,7 +23,7 @@ use encoded_ops::clz;
 use encoded_ops::rev;
 use encoded_ops::subs;
 
-use crate::REG_WIDTH;
+use crate::MAX_WIDTH;
 
 pub struct SolverCtx {
     smt: easy_smt::Context,
@@ -1678,7 +1678,7 @@ pub fn run_solver(
         dynwidths: true,
         onlywidths: false,
         tyctx: rule_sem.tyctx.clone(),
-        bitwidth: REG_WIDTH,
+        bitwidth: MAX_WIDTH,
         var_map: HashMap::new(),
         width_vars: HashMap::new(),
         width_assumptions: vec![],
@@ -1882,7 +1882,7 @@ pub fn run_solver_with_static_widths(
         dynwidths: false,
         onlywidths: false,
         tyctx: tyctx.clone(),
-        bitwidth: REG_WIDTH,
+        bitwidth: MAX_WIDTH,
         var_map: HashMap::new(),
         width_vars: HashMap::new(),
         width_assumptions: vec![],
@@ -1918,13 +1918,13 @@ pub fn run_solver_with_static_widths(
         (None, None) => {
             println!(
                 "Width of relevant bits of LHS and RHS unknown, using full register bitwidth: {}",
-                REG_WIDTH
+                MAX_WIDTH
             );
-            REG_WIDTH
+            MAX_WIDTH
         }
     };
 
-    let (lhs_care_bits, rhs_care_bits) = if width == REG_WIDTH {
+    let (lhs_care_bits, rhs_care_bits) = if width == MAX_WIDTH {
         (lhs, rhs)
     } else {
         (