1 files changed, 20 insertions, 0 deletions
diff --git a/test/Feature/LongDoubleSupport.c b/test/Feature/LongDoubleSupport.c
new file mode 100644
index 00000000..b4631832
--- /dev/null
+++ b/test/Feature/LongDoubleSupport.c
@@ -0,0 +1,20 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc > %t2.out
+
+#include <stdio.h>
+#include <float.h>
+
+// FIXME: This doesn't really work at all, it just doesn't
+// crash. Until we have wide constant support, that is all we care
+// about; the only reason this comes up is in initialization of
+// constants, we don't actually end up seeing much code which uses long
+// double.
+int main() {
+  long double a = LDBL_MAX;
+  long double b = -1;
+  long double c = a + b;
+  printf("a = %Lg\n", a);
+  printf("b = %Lg\n", b);
+  printf("c = %Lg\n", c);
+  return 0;
+}