about summary refs log tree commit diff homepage
path: root/test/Feature/SilentKleeAssume.c
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2015-12-11 14:24:34 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2015-12-11 14:24:34 +0000
commit9eddbdbddb0e21523dbbec5d21e64b79abcffb5c (patch)
tree0aad9ca9505e0ff01ea4bce103379c85e7f9d2a8 /test/Feature/SilentKleeAssume.c
parentee5a905cda1af731c3994e63f140c654c5dc7c2c (diff)
downloadklee-9eddbdbddb0e21523dbbec5d21e64b79abcffb5c.tar.gz
Change SilentKleeAssume.c test slightly so that
``--silent-klee-assume=0`` is no longer passed. This ensures that we
also check that ``--silent-klee-assume`` is off by default.
Diffstat (limited to 'test/Feature/SilentKleeAssume.c')
-rw-r--r--test/Feature/SilentKleeAssume.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/Feature/SilentKleeAssume.c b/test/Feature/SilentKleeAssume.c
index e444b6b9..59002f15 100644
--- a/test/Feature/SilentKleeAssume.c
+++ b/test/Feature/SilentKleeAssume.c
@@ -3,7 +3,7 @@
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --silent-klee-assume %t.bc > %t.silent-klee-assume.log 2>&1
 // RUN: FileCheck -input-file=%t.silent-klee-assume.log -check-prefix=CHECK-SILENT-KLEE-ASSUME %s
 // RUN: rm -rf %t.klee-out
-// RUN: not %klee --output-dir=%t.klee-out --exit-on-error --silent-klee-assume=0 %t.bc > %t.default-klee-assume.log 2>&1
+// RUN: not %klee --output-dir=%t.klee-out --exit-on-error %t.bc > %t.default-klee-assume.log 2>&1
 // RUN: FileCheck -input-file=%t.default-klee-assume.log -check-prefix=CHECK-DEFAULT-KLEE-ASSUME %s
 
 #include <stdio.h>