Skip to content

Commit 8dcd386

Browse files
author
Owen Jones
committed
Make test work again and turn it on
Three assumptions were missing. Now the test works and we can turn it back on.
1 parent 219b8bd commit 8dcd386

File tree

2 files changed

+4
-1
lines changed

2 files changed

+4
-1
lines changed

regression/cbmc/unsigned___int128/main.c

+3
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,9 @@ void reduce(
2929
__CPROVER_assume(in[1]<((widelimb)1<<126));
3030
__CPROVER_assume(in[2]<((widelimb)1<<126));
3131
__CPROVER_assume(in[3]<((widelimb)1<<126));
32+
__CPROVER_assume(in[4]<((widelimb)1<<126));
33+
__CPROVER_assume(in[5]<((widelimb)1<<126));
34+
__CPROVER_assume(in[6]<((widelimb)1<<126));
3235

3336
static const widelimb two127p15 = (((widelimb) 1) << 127) +
3437
(((widelimb) 1) << 15);

regression/cbmc/unsigned___int128/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--unsigned-overflow-check --signed-overflow-check --function reduce
44
^EXIT=0$

0 commit comments

Comments
 (0)