summaryrefslogtreecommitdiff
path: root/Test/houdini/houd12.bpl
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-27 20:53:49 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-27 20:53:49 +0100
commit02aca9ffab2d5a63e89f83d5eadb7133132c3b0a (patch)
tree673526b54101f72b42813d6f05edaba15f82b727 /Test/houdini/houd12.bpl
parent75416c24e78d9992c10fbb86ba458e813acf943d (diff)
Fix lit test suite when running Boogie under a path that contains
spaces.
Diffstat (limited to 'Test/houdini/houd12.bpl')
-rw-r--r--Test/houdini/houd12.bpl2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/houdini/houd12.bpl b/Test/houdini/houd12.bpl
index a3379a2e..7e39b8af 100644
--- a/Test/houdini/houd12.bpl
+++ b/Test/houdini/houd12.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment %s | %OutputCheck -d %s
+// RUN: %boogie -noinfer -contractInfer -printAssignment "%s" | %OutputCheck -d "%s"
// Example to test candidate annotations on loops
// CHECK-L: Assignment computed by Houdini: