summaryrefslogtreecommitdiff
path: root/Test/dafny0/runtest.bat
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-09-10 16:13:03 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-09-10 16:13:03 -0700
commitbef7f2ff0dbe833b157970efa16b12086776ef70 (patch)
tree78b2b8f6da0f312a72c60e3cfb9dd4ffa9a4e00f /Test/dafny0/runtest.bat
parent68d57324e25c44f022e55bbc55fffd4e22842928 (diff)
Dafny: improved checking of inherited postconditions (in refinements)
Diffstat (limited to 'Test/dafny0/runtest.bat')
-rw-r--r--Test/dafny0/runtest.bat6
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 --------------------