Added test case exposing division by zero failure reported by @kren1, and recently fixed in STP.

1 files changed, 23 insertions, 0 deletions

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);
+}