diff options
| author |  wuestholz <unknown> | 2013-05-30 09:12:51 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-05-30 09:12:51 -0700 |
| commit | d5574270cc5d424f1b3ec6a8021f9ef42c2c265b (patch) | |
| tree | 6798976ea948b72f95e9c21b858d40d9c8d1f7de /Source/VCGeneration | |
| parent | 84670125bef08609d4c447c27f245fef530ebcd2 (diff) | |
Changed the prover interface to report traces for time outs and out of memory.
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index cabc9d9e..dc9f496b 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -597,7 +597,7 @@ namespace VC { CounterexampleCollector collector = new CounterexampleCollector();
Outcome outcome = VerifyImplementation(impl, collector);
- if (outcome == Outcome.Errors) {
+ if (outcome == Outcome.Errors || outcome == Outcome.TimedOut || outcome == Outcome.OutOfMemory) {
errors = collector.examples;
} else {
errors = null;
|