new design for linear types + VCgen

ported all the examples
added the QED examples to runtest.bat

1 files changed, 3 insertions, 0 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 10becb3b..f30213a0 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -443,18 +443,21 @@ namespace Microsoft.Boogie
             {

                 var domainName = linearTypeChecker.FindDomainName(v);

                 if (domainName == null) continue;

+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 domainNameToScope[domainName].Add(v);

             }

             foreach (Variable v in first.thatInParams)

             {

                 var domainName = linearTypeChecker.FindDomainName(v);

                 if (domainName == null) continue;

+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 domainNameToScope[domainName].Add(v);

             }

             foreach (Variable v in second.thisInParams)

             {

                 var domainName = linearTypeChecker.FindDomainName(v);

                 if (domainName == null) continue;

+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 domainNameToScope[domainName].Add(v);

             }

             foreach (string domainName in domainNameToScope.Keys)