3 files changed, 42 insertions, 0 deletions
diff --git a/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery
new file mode 100644
index 00000000..9116ea47
--- /dev/null
+++ b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery
@@ -0,0 +1,15 @@
+# RUN: %kleaver %s 2>&1 | FileCheck %s
+array n_args[4] : w32 -> w8 = symbolic
+array n_args_1[4] : w32 -> w8 = symbolic
+array A-data-stat[144] : w32 -> w8 = symbolic
+array stdin-stat[144] : w32 -> w8 = symbolic
+(query [(Ult N0:(ReadLSB w32 0 n_args) 2)
+(Slt 0 N0)
+(Ult N1:(ReadLSB w32 0 n_args_1) 3)
+(Slt 0 N1)
+(Slt 1 N1)
+(Eq false (Eq 0 (And w64 (ReadLSB w64 8 A-data-stat) 2147483647)))
+(Ult (ReadLSB w64 56 A-data-stat) 65536)
+(Eq false (Eq 0 (And w64 (ReadLSB w64 8 stdin-stat) 2147483647)))]
+(Eq false (Ult (ReadLSB w64 56 stdin-stat) 65536)) [] [n_args])
+# CHECK: INVALID
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;
+} 
diff --git a/test/regression/lit.local.cfg b/test/regression/lit.local.cfg
new file mode 100644
index 00000000..d64daf29
--- /dev/null
+++ b/test/regression/lit.local.cfg
@@ -0,0 +1,2 @@
+# Look for .kquery files too
+config.suffixes.add('.kquery')