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;
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;