diff options
Diffstat (limited to 'test/regression/2014-09-13-debug-info.c')
| -rw-r--r-- | test/regression/2014-09-13-debug-info.c | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regression/2014-09-13-debug-info.c b/test/regression/2014-09-13-debug-info.c index ddf8461d..e4e9874c 100644 --- a/test/regression/2014-09-13-debug-info.c +++ b/test/regression/2014-09-13-debug-info.c @@ -8,7 +8,7 @@ // one with the prefered CEX. We verify this by using ktest-tool to dump the // values, and then checking the output. // -// RUN: /bin/sh -c "ktest-tool --write-int %t.klee-out/*.ktest" | sort > %t.data-values +// RUN: /bin/sh -c "ktest-tool %t.klee-out/*.ktest" | sort > %t.data-values // RUN: FileCheck < %t.data-values %s // CHECK: object 0: data: 0 |