diff options
| author |  tabarbe <unknown> | 2010-08-12 22:30:57 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-12 22:30:57 +0000 |
| commit | e7cf2c7763bb20e7090d3cc5f3f8fbe804a69453 (patch) | |
| tree | 29d576dce4e7d27693dc0e9c2cd8e0d49de5fd13 /Test/sanity | |
| parent | 3895897f97d2234533a23f0e99e95af73e8f0734 (diff) | |
Boogie: This reg test was not running verification.
Diffstat (limited to 'Test/sanity')
| -rw-r--r-- | Test/sanity/runtest.bat | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/sanity/runtest.bat b/Test/sanity/runtest.bat index f05e832e..8b790109 100644 --- a/Test/sanity/runtest.bat +++ b/Test/sanity/runtest.bat @@ -5,5 +5,5 @@ set BOOGIEDIR=..\..\Binaries set BGEXE=%BOOGIEDIR%\Boogie.exe
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-%BGEXE% %* /noVerify ..\textbook\bubble.bpl
+%BGEXE% %* ..\textbook\bubble.bpl
%DAFNY_EXE% /compile:0 %* ..\dafny1\Celebrity.dfy
\ No newline at end of file |