From d314c08878519e11797bc63067804e3b379e0596 Mon Sep 17 00:00:00 2001
From: Reini Urban <reini.urban@gmail.com>
Date: Wed, 21 Feb 2024 08:04:26 +0100
Subject: [PATCH] cbmc: better set.find_range test

---
 tests/verify/set-1.c | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/verify/set-1.c b/tests/verify/set-1.c
index 69fbd45a..6e476b55 100644
--- a/tests/verify/set-1.c
+++ b/tests/verify/set-1.c
@@ -36,7 +36,9 @@ int main()
     set_int_it pos = set_int_begin(&a);
     set_int_find_range(&pos, a1);
 #ifdef CBMC
-    pos->end = nondet_int();
+    pos->begin = nondet_uint();
+    pos->end = nondet_uint();
+    _CPROVER_assume (pos->begin <= pos->end);
 #endif
     set_int_find_range(&pos, a1);
     set_int_erase_it(&pos);