diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-18 16:41:10 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-18 16:41:10 -0700 |
| commit | a019d797bd42866242e48ef00850f74e3bdc9241 (patch) | |
| tree | 5ff143def292fcf8190c2613fb675fa19692ab81 /Source/DafnyServer/VerificationTask.cs | |
| parent | ac137091eac412d2ea8a79ac1c05d161db3365f2 (diff) | |
Server: disable tracing when running tests, and fix an encoding issue.
z3 doesn't support byte-order marks; thus using the default UTF8Encoding object
(to allow printing nice warning signs) causes issues, as it sends a BOM before
anything else.
Diffstat (limited to 'Source/DafnyServer/VerificationTask.cs')
| -rw-r--r-- | Source/DafnyServer/VerificationTask.cs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs index a00688b1..dbafc781 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();
+ task.Run(false);
Interaction.EOM(Interaction.SUCCESS, null);
} catch (Exception ex) {
Interaction.EOM(Interaction.FAILURE, ex);
}
}
- internal void Run() {
- ServerUtils.ApplyArgs(args);
+ internal void Run(bool trace = true) {
+ ServerUtils.ApplyArgs(args, trace);
new DafnyHelper(filename, ProgramSource).Verify();
}
}
|