1 files changed, 18 insertions, 0 deletions
diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c
new file mode 100644
index 00000000..d73b6076
--- /dev/null
+++ b/test/Feature/PreferCex.c
@@ -0,0 +1,18 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+// RUN: klee-bout-tool klee-last/test000001.bout | grep -F 'Hi\x00\x00'
+
+#include <assert.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+int main() {
+  char buf[4];
+
+  klee_make_symbolic(buf, sizeof buf);
+  klee_prefer_cex(buf, buf[0]=='H');
+  klee_prefer_cex(buf, buf[1]=='i');
+  klee_prefer_cex(buf, buf[2]=='\0');
+
+  return 0;
+}