From 96f9f0c9e41b5d4957faf78bcadb3957e52e1632 Mon Sep 17 00:00:00 2001
From: Evan Johnson <e5johnso@eng.ucsd.edu>
Date: Mon, 22 Jul 2024 10:59:19 -0700
Subject: [PATCH] reorder short-circuiting comparison to make proof go through

---
 arch/rv32i/src/pmp.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/arch/rv32i/src/pmp.rs b/arch/rv32i/src/pmp.rs
index a19c8282a2..052553358a 100644
--- a/arch/rv32i/src/pmp.rs
+++ b/arch/rv32i/src/pmp.rs
@@ -132,8 +132,8 @@ impl NAPOTRegionSpec {
     /// [`NAPOTRegionSpec`]'s documentation are satisfied, otherwise `None`.
     // #[flux::ignore]
     pub fn new(start: *const u8, size: usize) -> Option<Self> {
-        assume(size > 0); // I thought the struct has already refined this property?
-        if !size.is_power_of_two() || (start as usize) % size != 0 || size < 8 {
+        //assume(size > 0); // I thought the struct has already refined this property?
+        if size < 8 || !size.is_power_of_two() || (start as usize) % size != 0  {
             None
         } else {
             Some(NAPOTRegionSpec { start, size })