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

2 files changed, 0 insertions, 5 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 8c8b17a0..11db59b0 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -3621,7 +3621,6 @@ namespace VC {
                         Hashtable/*<int, Absy!>*/ label2absy,

                         ProverContext proverCtxt) {

       Contract.Requires(startBlock != null);

-      Contract.Requires(label2absy != null);

       Contract.Requires(proverCtxt != null);

 

       Contract.Ensures(Contract.Result<VCExpr>() != null);

@@ -3640,7 +3639,6 @@ namespace VC {
                         ProverContext proverCtxt)

     {

       Contract.Requires(block != null);

-      Contract.Requires(label2absy != null);

       Contract.Requires(blockVariables!= null);

       Contract.Requires(cce.NonNullElements(bindings));

       Contract.Requires(proverCtxt != null);

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;