From 9fe07e99403ad76ffa4654140fcb9203a54c8572 Mon Sep 17 00:00:00 2001
From: Necromaticon <54175362+Necromaticon@users.noreply.github.com>
Date: Thu, 18 Apr 2024 13:09:57 +0200
Subject: [PATCH 1/2] Update gauss_sum_nondet.rs

Issue with the initial nondet value being out of the assumed bounds
---
 benchmarks/smack-regressions/loops/gauss_sum_nondet.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/benchmarks/smack-regressions/loops/gauss_sum_nondet.rs b/benchmarks/smack-regressions/loops/gauss_sum_nondet.rs
index 87e6068..3284d58 100644
--- a/benchmarks/smack-regressions/loops/gauss_sum_nondet.rs
+++ b/benchmarks/smack-regressions/loops/gauss_sum_nondet.rs
@@ -3,7 +3,7 @@
 
 pub fn main() {
     let mut sum = 0;
-    let b = verifier::nondet!(7u64);
+    let b = verifier::nondet!(4u64);
     verifier::assume!(b < 5 && b > 1);
     for i in 0..b as u64 {
         sum += i;

From bbed69bd67a1fb9ad9fe66cd8d8792f1fb886e02 Mon Sep 17 00:00:00 2001
From: Necromaticon <54175362+Necromaticon@users.noreply.github.com>
Date: Thu, 18 Apr 2024 13:10:24 +0200
Subject: [PATCH 2/2] Update iterator.rs

Issue with the initial nondet value being out of the assumed bounds
---
 benchmarks/smack-regressions/loops/iterator.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/benchmarks/smack-regressions/loops/iterator.rs b/benchmarks/smack-regressions/loops/iterator.rs
index 98f41da..54a7932 100644
--- a/benchmarks/smack-regressions/loops/iterator.rs
+++ b/benchmarks/smack-regressions/loops/iterator.rs
@@ -11,7 +11,7 @@ fn fac(n: u64) -> u64 {
 
 pub fn main() {
     let mut a = 1;
-    let n = verifier::nondet!(6u64);
+    let n = verifier::nondet!(4u64);
     verifier::assume!(n < 5);
     for i in 1..n + 1 as u64 {
         a *= i;