diff --git a/silver b/silver
index e72250fb1..11ab30d84 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit e72250fb1da0aac8b9b7ff3ac2a75142bf59ee3a
+Subproject commit 11ab30d8402a51fca41846ab88f514af6fb53170
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index cb3fe8713..6c4838890 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -778,7 +778,16 @@ object evaluator extends EvaluationRules {
               val snap1 = snap.convert(sorts.Snap)
               val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
               v3.decider.assume(preFApp)
-              val tFApp = App(v3.symbolConverter.toFunction(func), snap1 :: tArgs)
+              val funcAnn = func.info.getUniqueInfo[AnnotationInfo]
+              val tFApp = funcAnn match {
+                case Some(a) if a.values.contains("opaque") =>
+                  val funcAppAnn = fapp.info.getUniqueInfo[AnnotationInfo]
+                  funcAppAnn match {
+                    case Some(a) if a.values.contains("reveal") => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs)
+                    case _ => App(functionSupporter.limitedVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
+                  }
+                case _ => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs)
+              }
               val fr5 =
                 s4.functionRecorder.changeDepthBy(-1)
                                    .recordSnapshot(fapp, v3.decider.pcs.branchConditions, snap1)
diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala
index 98958fc71..1861587c1 100644
--- a/src/main/scala/supporters/functions/FunctionData.scala
+++ b/src/main/scala/supporters/functions/FunctionData.scala
@@ -259,9 +259,13 @@ class FunctionData(val programFunction: ast.Function,
       val pre = preconditionFunctionApplication
       val nestedDefinitionalAxioms = generateNestedDefinitionalAxioms
       val body = And(nestedDefinitionalAxioms ++ List(Implies(pre, And(BuiltinEquals(functionApplication, translatedBody)))))
+      val funcAnn = programFunction.info.getUniqueInfo[ast.AnnotationInfo]
+      val actualPredicateTriggers = funcAnn match {
+        case Some(a) if a.values.contains("opaque") => Seq()
+        case _ => predicateTriggers.values.map(pt => Trigger(Seq(triggerFunctionApplication, pt)))
+      }
       val allTriggers = (
-           Seq(Trigger(functionApplication))
-        ++ predicateTriggers.values.map(pt => Trigger(Seq(triggerFunctionApplication, pt))))
+           Seq(Trigger(functionApplication)) ++ actualPredicateTriggers)
 
       Forall(arguments, body, allTriggers)})
   }
diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
index 81aa923a1..5235f31de 100644
--- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
+++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
@@ -15,6 +15,7 @@ import viper.silicon.rules.functionSupporter
 import viper.silicon.state.{Identifier, SimpleIdentifier, SuffixedIdentifier, SymbolConverter}
 import viper.silicon.state.terms._
 import viper.silicon.supporters.ExpressionTranslator
+import viper.silver.ast.AnnotationInfo
 import viper.silver.reporter.{InternalWarningMessage, Reporter}
 
 class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
@@ -127,7 +128,16 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
 
       case eFApp: ast.FuncApp =>
         val silverFunc = program.findFunction(eFApp.funcname)
-        val fun = symbolConverter.toFunction(silverFunc)
+        val funcAnn = silverFunc.info.getUniqueInfo[AnnotationInfo]
+        val fun = funcAnn match {
+          case Some(a) if a.values.contains("opaque") =>
+            val funcAppAnn = eFApp.info.getUniqueInfo[AnnotationInfo]
+            funcAppAnn match {
+              case Some(a) if a.values.contains("reveal") => symbolConverter.toFunction(silverFunc)
+              case _ => functionSupporter.limitedVersion(symbolConverter.toFunction(silverFunc))
+            }
+          case _ => symbolConverter.toFunction(silverFunc)
+        }
         val args = eFApp.args map (arg => translate(arg))
         val snap = getOrFail(data.fappToSnap, eFApp, sorts.Snap)
         val fapp = App(fun, snap +: args)