Fix contracts so runtime checking can be turned on.

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 5323bb03..20b17e6b 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -507,8 +507,8 @@ namespace VC {
     public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {

       Contract.Requires(impl != null);

       Contract.Requires(program != null);

-      Contract.Requires(Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));

 

+      Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));

       Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       Helpers.ExtraTraceInformation("Starting implementation verification");