Skip to content

Commit 748bb00

Browse files
author
Daniel Kroening
committed
avoid floating-point arithmetic in fixed-point test
1 parent 4714c4e commit 748bb00

File tree

1 file changed

+2
-2
lines changed
  • regression/cbmc/Fixedbv1

1 file changed

+2
-2
lines changed

regression/cbmc/Fixedbv1/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,13 @@ int main() {
55
int y;
66

77
x=2;
8-
x-=0.6;
8+
x -= (__CPROVER_fixedbv[64][32])0.6;
99
y=x; // this yields 1.4, which is cut off
1010

1111
assert(y==1);
1212

1313
x=2;
14-
x-=0.4;
14+
x -= (__CPROVER_fixedbv[64][32])0.4;
1515
y=x; // this yields 1.6, which is cut off, too!
1616

1717
assert(y==1);

0 commit comments

Comments
 (0)