Skip to content

Commit d314c08

Browse files
committed
cbmc: better set.find_range test
1 parent 3b7df3a commit d314c08

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

tests/verify/set-1.c

+3-1
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,9 @@ int main()
3636
set_int_it pos = set_int_begin(&a);
3737
set_int_find_range(&pos, a1);
3838
#ifdef CBMC
39-
pos->end = nondet_int();
39+
pos->begin = nondet_uint();
40+
pos->end = nondet_uint();
41+
_CPROVER_assume (pos->begin <= pos->end);
4042
#endif
4143
set_int_find_range(&pos, a1);
4244
set_int_erase_it(&pos);

0 commit comments

Comments
 (0)