diff options
| author |  MichalMoskal <unknown> | 2011-02-02 02:17:11 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-02 02:17:11 +0000 |
| commit | cda903372df528488421f2f7dee66d3c5b639360 (patch) | |
| tree | eabe237fef8397d1d7350087b0ea6ab588d7d73d /Source/VCGeneration/VC.cs | |
| parent | 7f7cf6ccc734f4f380db06cb15f1092c5293002e (diff) | |
Don't treat "Inconclusive" answer as fatal when splitting.
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 54bd5358..87f78a96 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1380,7 +1380,6 @@ namespace VC { cur_outcome = Outcome.TimedOut;
return;
case ProverInterface.Outcome.Undetermined:
- prover_failed = true;
if (cur_outcome != Outcome.Errors)
cur_outcome = Outcome.Inconclusive;
return;
@@ -1694,7 +1693,7 @@ namespace VC { break;
}
- Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors);
+ Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
}
if (prover_failed) {
|