diff options
Diffstat (limited to 'test/regression/2020-01-14-fabs-compare.c')
-rw-r--r-- | test/regression/2020-01-14-fabs-compare.c | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regression/2020-01-14-fabs-compare.c b/test/regression/2020-01-14-fabs-compare.c new file mode 100644 index 00000000..563a6609 --- /dev/null +++ b/test/regression/2020-01-14-fabs-compare.c @@ -0,0 +1,16 @@ +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --exit-on-error --output-dir=%t.klee-out %t.bc + +#include <math.h> +#include <assert.h> + +int main(void) { + long double a = 0.25; + long double b = -a; + + long double b_abs = fabsl(b); + + assert(a == b_abs); + return 0; +} |