Added test case with the examples from https://github.com/klee/klee/issues/334, which triggers a bug in solver-optimize-divides, and which is for now expected to fail.

1 files changed, 25 insertions, 0 deletions

diff --git a/test/regression/2016-04-14-sdiv-2.c b/test/regression/2016-04-14-sdiv-2.c
new file mode 100644
index 00000000..88a5fca3
--- /dev/null
+++ b/test/regression/2016-04-14-sdiv-2.c
@@ -0,0 +1,25 @@
+// XFAIL: *
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=true %t.bc >%t1.log
+// RUN: grep "m is 2" %t1.log
+
+#include <assert.h>
+
+int main(void)
+{
+  int n, m;
+  klee_make_symbolic(&n, sizeof n, "n");
+  klee_assume(n < -1);
+
+  if (n/2 > 0)
+    assert(0);
+
+  klee_make_symbolic(&m, sizeof m, "m");
+  klee_assume(m > 0);
+
+  if (m/2 == 2)
+    printf("m is 2\n");
+  
+  return 0;
+}