Merge pull request #679 from viperproject/meilers_issue_678

Fix for issue #678

Author: marcoeilers

silver

@@ -34,8 +34,11 @@ class DefaultSetsContributor(val domainTranslator: DomainsTranslator[Term], conf
      *       However, it is currently not (easily) possible for the latter to contribute instances
      *       of set axioms.
      */
-    if (program.existsDefined { case f: ast.Forall if (f.triggers flatMap (_.exps)) exists (e => e.existsDefined { case _: ast.ResourceAccess => }) =>
-      case q: ast.QuantifiedExp if !q.isPure => }) {
+    if (program.existsDefined {
+      case f: ast.Forall if (f.triggers flatMap (_.exps)) exists (e => e.existsDefined { case _: ast.ResourceAccess => }) =>
+      case q: ast.Exists if (q.triggers flatMap (_.exps)) exists (e => e.existsDefined { case _: ast.ResourceAccess => }) =>
+      case q: ast.QuantifiedExp if !q.isPure =>
+    }) {
       program.fields foreach {f => setTypeInstances += ast.SetType(f.typ)}
 
       setTypeInstances += ast.SetType(ast.Ref) /* $FVF.domain_f is of type Set[Ref] */

src/main/scala/supporters/DefaultSetsContributor.scala

@@ -14,7 +14,7 @@ import viper.silicon.interfaces.{PreambleContributor, PreambleReader}
 import viper.silicon.interfaces.decider.{ProverLike, TermConverter}
 import viper.silicon.state.SymbolConverter
 import viper.silicon.state.terms.{SortDecl, sorts}
-import viper.silver.ast.{FieldAccess, Forall}
+import viper.silver.ast.{Exists, FieldAccess, Forall}
 
 trait FieldValueFunctionsContributor[SO, SY, AX] extends PreambleContributor[SO, SY, AX]
 
@@ -55,6 +55,10 @@ class DefaultFieldValueFunctionsContributor(preambleReader: PreambleReader[Strin
         val trigExps = triggers flatMap (_.exps)
         val fieldAccesses = trigExps flatMap (e => e.deepCollect {case fa: FieldAccess => fa})
         collectedFields ++= (fieldAccesses map (_.field))
+      case Exists(_, triggers, _) =>
+        val trigExps = triggers flatMap (_.exps)
+        val fieldAccesses = trigExps flatMap (e => e.deepCollect { case fa: FieldAccess => fa })
+        collectedFields ++= (fieldAccesses map (_.field))
     }
 
     // WARNING: DefaultSetsContributor contributes a sort that is due to QPs over fields

src/main/scala/supporters/qps/FieldValueFunctionsContributor.scala

@@ -85,6 +85,10 @@ class DefaultPredicateAndWandSnapFunctionsContributor(preambleReader: PreambleRe
         val trigExps = triggers flatMap (_.exps)
         val predicateAccesses = trigExps flatMap (e => e.deepCollect {case pa: PredicateAccess => pa})
         collectedPredicates ++= (predicateAccesses map (_.loc(program)))
+      case ast.Exists(_, triggers, _) =>
+        val trigExps = triggers flatMap (_.exps)
+        val predicateAccesses = trigExps flatMap (e => e.deepCollect { case pa: PredicateAccess => pa })
+        collectedPredicates ++= (predicateAccesses map (_.loc(program)))
     }
 
     collectedWandIdentifiers =