diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 16:13:03 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 16:13:03 -0700 |
| commit | bef7f2ff0dbe833b157970efa16b12086776ef70 (patch) | |
| tree | 78b2b8f6da0f312a72c60e3cfb9dd4ffa9a4e00f /Test/dafny0/runtest.bat | |
| parent | 68d57324e25c44f022e55bbc55fffd4e22842928 (diff) | |
Dafny: improved checking of inherited postconditions (in refinements)
Diffstat (limited to 'Test/dafny0/runtest.bat')
| -rw-r--r-- | Test/dafny0/runtest.bat | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 1ccb292c..2055e283 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -29,6 +29,12 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
)
+for %%f in (Superposition.dfy) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp /tracePOs %* %%f
+)
+
for %%f in (SmallTests.dfy LetExpr.dfy) do (
echo.
echo -------------------- %%f --------------------
|