Fix for secureVCGen

1 files changed, 3 insertions, 0 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 6f8d3668..e88eb55e 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2609,6 +2609,9 @@ namespace VC {
           if(impl.LocVars.Any(v => isVisible(v)))

               throw new InvalidProgramForSecureVc("SecureVc: Visible Local variables not allowed");

 

+          // Desugar procedure calls

+          DesugarCalls(impl);

+

           // Gather spec, remove existing ensures

           var secureAsserts = new List<AssertCmd>();

           var logicalAsserts = new List<AssertCmd>();