2 files changed, 26 insertions, 1 deletions
diff --git a/test/Coverage/ReplayOutDir.c b/test/Coverage/ReplayOutDir.c
index ca7e590a..d9bffea0 100644
--- a/test/Coverage/ReplayOutDir.c
+++ b/test/Coverage/ReplayOutDir.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: rm -rf %t1.out %t1.replay
 // RUN: %klee --output-dir=%t1.out %t1.bc
-// RUN: %klee --output-dir=%t1.replay --replay-out-dir=%t1.out %t1.bc
+// RUN: %klee --output-dir=%t1.replay --replay-ktest-dir=%t1.out %t1.bc
 
 int main() {
   int i;
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;
+}