LetVC can get null label2absy from lazy inlining. So, I weakened the precondition otherwise the checked build was failing

1 files changed, 0 insertions, 3 deletions

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 23be6082..f5469ebf 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -17,7 +17,6 @@ namespace VC {
     [ContractInvariantMethod]

     void ObjectInvariant() 

     {

-      Contract.Invariant(Label2absy!=null);

       Contract.Invariant(Ctxt != null);

     }

 

@@ -27,7 +26,6 @@ namespace VC {
     

     public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt)

     {

-      Contract.Requires(label2absy != null);

       Contract.Requires(ctxt != null);

       this.Label2absy = label2absy;

       this.Ctxt = ctxt;

@@ -36,7 +34,6 @@ namespace VC {
     

     public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt, Variable controlFlowVariable)

     {

-      Contract.Requires(label2absy != null);

       Contract.Requires(ctxt != null);

       this.Label2absy = label2absy;

       this.Ctxt = ctxt;