[Civl] Improvements to pool-based quantifier instantiation

Source/Core/base.bpl

@@ -320,8 +320,9 @@ pure procedure {:inline 1} Map_Assume<K,V>({:linear} src: Map K V, {:linear} dst
 
 type Loc _;
 
-pure procedure {:inline 1} One_New<V>() returns ({:linear} l: One (Loc V))
+pure procedure {:inline 1} One_New<V>() returns ({:linear} {:pool "One_New"} l: One (Loc V))
 {
+  assume {:add_to_pool "One_New", l} true;
 }
 
 procedure create_async<T>(PA: T);

Source/VCExpr/QuantifierInstantiationEngine.cs

@@ -51,7 +51,7 @@ public QuantifierInstantiationInfo(Dictionary<VCExprVar, HashSet<string>> boundV
     private string skolemConstantNamePrefix;
     internal VCExpressionGenerator vcExprGen;
     private Boogie2VCExprTranslator exprTranslator;
-    internal static ConcurrentDictionary<string, Type> labelToType = new();
+    internal static ConcurrentDictionary<string, HashSet<Type>> labelToTypes = new(); // pool name may map to multiple types
 
     public static VCExpr Instantiate(Implementation impl, VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr)
     {
@@ -199,18 +199,11 @@ public static HashSet<string> FindInstantiationHints(Variable v)
             if (x is string poolName)
             {
               labels.Add(poolName);
-              if (labelToType.ContainsKey(poolName))
+              if (!labelToTypes.ContainsKey(poolName))
               {
-                if (!v.TypedIdent.Type.Equals(labelToType[poolName]))
-                {
-                  Console.WriteLine(
-                    $"{tok.filename}({tok.line},{tok.col}): conflicting type for pool {poolName} used earlier with type {labelToType[poolName]}");
-                }
-              }
-              else
-              {
-                labelToType[poolName] = v.TypedIdent.Type;
+                labelToTypes[poolName] = new();
               }
+              labelToTypes[poolName].Add(v.TypedIdent.Type);
             }
             else
             {
@@ -457,6 +450,16 @@ private void InstantiateQuantifierAtInstance(VCExprQuantifier quantifierExpr, Li
       {
         return;
       }
+
+      // Since a pool name may be used with multiple types, we have to prune invalid instances
+      for (int i = 0; i < quantifierExpr.BoundVars.Count; i++)
+      {
+        if (!quantifierExpr.BoundVars[i].Type.Equals(instance[i].Type))
+        {
+          return;
+        }
+      }
+
       var subst = new VCExprSubstitution(
         Enumerable.Range(0, quantifierExpr.BoundVars.Count).ToDictionary(
           x => quantifierExpr.BoundVars[x],
@@ -852,20 +855,16 @@ private void FindInstantiationSources(ICarriesAttributes o)
       {
         if (iter.Key == "add_to_pool")
         {
-          if (iter.Params[0] is string poolName && QuantifierInstantiationEngine.labelToType.ContainsKey(poolName))
+          if (iter.Params[0] is string poolName && QuantifierInstantiationEngine.labelToTypes.ContainsKey(poolName))
           {
             var tok = iter.tok;
-            var type = QuantifierInstantiationEngine.labelToType[poolName];
+            var poolTypes = QuantifierInstantiationEngine.labelToTypes[poolName];
             iter.Params.Skip(1).ForEach(x =>
             {
-              if (x is Expr e && e.Type.Equals(type))
+              if (x is Expr e && poolTypes.Contains(e.Type))
               {
                 hasInstances = true;
               }
-              else
-              {
-                Console.WriteLine($"{tok.filename}({tok.line},{tok.col}): expected expression of type {type}");
-              }
             });
           }
         }

Test/civl/samples/treiber-stack.bpl

@@ -138,7 +138,9 @@ modifies ts;
   var {:linear} stack: Map (Loc (Node X)) (Node X);
   var {:linear} one_loc_n: One (Loc (Node X));
 
-  if (success) {
+  success := false;
+  if (*) {
+    success := true;
     call one_loc_t, treiber := Map_Get(ts, loc_t);
     Treiber(top, stack) := treiber;
     call one_loc_n := One_New();