2 files changed, 26 insertions, 2 deletions
diff --git a/test/regression/2016-04-14-sdiv-2.c_ b/test/regression/2016-04-14-sdiv-2.c
index 88a5fca3..974036ee 100644
--- a/test/regression/2016-04-14-sdiv-2.c_
+++ b/test/regression/2016-04-14-sdiv-2.c
@@ -1,10 +1,11 @@
-// 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>
+#include <stdio.h>
+
+#include "klee/klee.h"
 
 int main(void)
 {
diff --git a/test/regression/2016-06-28-div-zero-bug.c b/test/regression/2016-06-28-div-zero-bug.c
new file mode 100644
index 00000000..11689aa0
--- /dev/null
+++ b/test/regression/2016-06-28-div-zero-bug.c
@@ -0,0 +1,23 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false %t.bc >%t1.log
+
+// This bug is triggered when using STP up to an including 2.1.0
+// See https://github.com/klee/klee/issues/308
+// and https://github.com/stp/stp/issues/206
+
+int b, a, g;
+
+int *c = &b, *d = &b, *f = &a;
+
+int safe_div(short p1, int p2) { 
+  return p2 == 0 ? p1 : p2; 
+}
+
+int main() {
+  klee_make_symbolic(&b, sizeof b);
+  if (safe_div(*c, 0))
+    *f = (int)&b % *c;
+
+  safe_div(a && g, *d);
+}