Allow to generate initial values with empty constraint set

1 files changed, 22 insertions, 0 deletions

diff --git a/test/regression/2015-08-30-empty-constraints.c b/test/regression/2015-08-30-empty-constraints.c
new file mode 100644
index 00000000..81439e21
--- /dev/null
+++ b/test/regression/2015-08-30-empty-constraints.c
@@ -0,0 +1,22 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t.bc 2> %t.log
+// RUN: FileCheck -input-file=%t.log %s
+
+/**
+ * This test generates one execution state without constraints.
+ *
+ * The state gets terminated (in this case return) and initial values
+ * are generated.
+ * Make sure we are able to generate an input.
+ */
+int main() {
+  int d;
+
+  klee_make_symbolic( &d, sizeof(d) );
+
+  // CHECK-NOT: unable to compute initial values (invalid constraints?)!
+  if ((d & 2) / 4)
+    return 1;
+  return 0;
+}