summaryrefslogtreecommitdiff
path: root/Source/DafnyServer/VerificationTask.cs
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-19 16:15:26 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-19 16:15:26 -0700
commit43cbd76e07262d05434e36dff99f8d10eb59a773 (patch)
tree7f2a878e755db64d193530fe9e8f78f15b20b100 /Source/DafnyServer/VerificationTask.cs
parent2f5d59592c5930c32039855824cc49983f643641 (diff)
Use /tracePO instead of /trace in the server
This removes the need for special treatment of test input (/trace includes timings in the output, which are not suitable for tests. /tracePO does not)
Diffstat (limited to 'Source/DafnyServer/VerificationTask.cs')
-rw-r--r--Source/DafnyServer/VerificationTask.cs6
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs
index dbafc781..a00688b1 100644
--- a/Source/DafnyServer/VerificationTask.cs
+++ b/Source/DafnyServer/VerificationTask.cs
@@ -44,15 +44,15 @@ namespace Microsoft.Dafny {
source = "method selftest() { assert true; }"
};
try {
- task.Run(false);
+ task.Run();
Interaction.EOM(Interaction.SUCCESS, null);
} catch (Exception ex) {
Interaction.EOM(Interaction.FAILURE, ex);
}
}
- internal void Run(bool trace = true) {
- ServerUtils.ApplyArgs(args, trace);
+ internal void Run() {
+ ServerUtils.ApplyArgs(args);
new DafnyHelper(filename, ProgramSource).Verify();
}
}