cbmc: better set.find_range test

rurban · Feb 21, 2024 · d314c08 · d314c08
1 parent 3b7df3a
commit d314c08
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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);