diff options
| author |  rustanleino <unknown> | 2010-05-21 18:38:47 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-05-21 18:38:47 +0000 |
| commit | 2fc9a47b200589fae14f698e7546553a0b31aec2 (patch) | |
| tree | ae0fd61bcd66c4f92833c33f82de518a718bfb7c /Source/DafnyDriver | |
| parent | 9657b7042a5a55fe96bc9b7560c473876d7efa60 (diff) | |
Dafny:
* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.ssc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.ssc b/Source/DafnyDriver/DafnyDriver.ssc index f6e10e59..8920db94 100644 --- a/Source/DafnyDriver/DafnyDriver.ssc +++ b/Source/DafnyDriver/DafnyDriver.ssc @@ -230,7 +230,7 @@ namespace Microsoft.Boogie PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, null/*new ErrorReporter()*/, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
switch (oc) {
case PipelineOutcome.VerificationCompleted:
- if (CommandLineOptions.Clo.Compile) {
+ if (CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) {
string targetFilename = "out.cs";
using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
Dafny.Compiler compiler = new Dafny.Compiler(target);
|