From b2230000f7364ea23cbb1ce16cb16fc130e3f6fe Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 1 Nov 2023 16:13:11 +0100
Subject: [PATCH] Disable predicate triggers for opaque functions

---
 silver                                                     | 2 +-
 .../viper/carbon/modules/impls/DefaultFuncPredModule.scala | 7 ++++++-
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/silver b/silver
index 315fb241..62dacc0f 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 315fb2418b4776962ce99ce3469f5f3896ec787e
+Subproject commit 62dacc0f71d4204a6f6261ec12e008e40a13c91d
diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala
index f47a235e..eab2c6c7 100644
--- a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala
+++ b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala
@@ -297,10 +297,15 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
         case _ => None}.flatten
     }
 
+    // Do not use predicate triggers if the function is annotated as opaque
+    val usePredicateTriggers = f.info.getUniqueInfo[sil.AnnotationInfo] match {
+      case Some(ai) if ai.values.contains("opaque") => false
+      case _ => true
+    }
 
     Axiom(Forall(
       stateModule.staticStateContributions() ++ args,
-      Seq(Trigger(Seq(staticGoodState,fapp))) ++ (if (predicateTriggers.isEmpty) Seq()  else Seq(Trigger(Seq(staticGoodState, triggerFuncStatelessApp(f,args map (_.l))) ++ predicateTriggers))),
+      Seq(Trigger(Seq(staticGoodState,fapp))) ++ (if (!usePredicateTriggers || predicateTriggers.isEmpty) Seq()  else Seq(Trigger(Seq(staticGoodState, triggerFuncStatelessApp(f,args map (_.l))) ++ predicateTriggers))),
       (staticGoodState && assumeFunctionsAbove(height)) ==>
         (precondition ==> (fapp === body))
     ))