diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/Feature/RewriteEqualities.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test/Feature/RewriteEqualities.c b/test/Feature/RewriteEqualities.c index 6bf199f7..b3cc0ef7 100644 --- a/test/Feature/RewriteEqualities.c +++ b/test/Feature/RewriteEqualities.c @@ -5,7 +5,7 @@ // RUN: grep "N0)" %t.klee-out/test000003.kquery // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --search=dfs --write-kqueries --rewrite-equalities %t.bc -// RUN: grep "(Read w8 8 const_arr1)" %t.klee-out/test000003.kquery +// RUN: FileCheck -input-file=%t.klee-out/test000003.kquery %s #include <stdio.h> #include <klee/klee.h> @@ -19,6 +19,8 @@ int run(unsigned char * x, unsigned char * y) { if(y[x[2]] < 11){ if(x[2] == 8){ + // CHECK: (query [(Eq 8 (Read w8 2 x))] + // CHECK-NEXT: false) return 2; } else{ return 3; |