diff --git a/src/main/scala/viper/gobra/translator/transformers/hyper/SIFError.scala b/src/main/scala/viper/gobra/translator/transformers/hyper/SIFError.scala
index 18c8562ca..5a3ec9dd2 100644
--- a/src/main/scala/viper/gobra/translator/transformers/hyper/SIFError.scala
+++ b/src/main/scala/viper/gobra/translator/transformers/hyper/SIFError.scala
@@ -12,7 +12,7 @@ import viper.silver.verifier._
 
 
 case class SIFTerminationChannelCheckFailed(offendingNode: ErrorNode, reason: ErrorReason,
-                                            override val cached: Boolean = false) extends AbstractVerificationError {
+                                            override val cached: Boolean = false) extends ExtensionAbstractVerificationError {
   val id: String = "termination_channel_check.failed"
   val text: String = "Termination channel might exist."
   override def withNode(offendingNode: ErrorNode = this.offendingNode): ErrorMessage =
@@ -21,7 +21,7 @@ case class SIFTerminationChannelCheckFailed(offendingNode: ErrorNode, reason: Er
   override def withReason(r: ErrorReason): AbstractVerificationError = SIFTerminationChannelCheckFailed(offendingNode, r)
 }
 
-case class SIFFoldNotLow(offendingNode: Fold) extends AbstractErrorReason {
+case class SIFFoldNotLow(offendingNode: Fold) extends ExtensionAbstractErrorReason {
   val id: String = "sif.fold"
   val readableMessage: String = s"The low parts of predicate ${offendingNode.acc.loc.predicateName} might not hold."
 
@@ -29,7 +29,7 @@ case class SIFFoldNotLow(offendingNode: Fold) extends AbstractErrorReason {
     SIFFoldNotLow(offendingNode.asInstanceOf[Fold])
 }
 
-case class SIFUnfoldNotLow(offendingNode: Unfold) extends AbstractErrorReason {
+case class SIFUnfoldNotLow(offendingNode: Unfold) extends ExtensionAbstractErrorReason {
   val id: String = "sif.unfold"
   val readableMessage: String = s"The low parts of predicate ${offendingNode.acc.loc.predicateName} might not hold."
 
@@ -37,7 +37,7 @@ case class SIFUnfoldNotLow(offendingNode: Unfold) extends AbstractErrorReason {
     SIFUnfoldNotLow(offendingNode.asInstanceOf[Unfold])
 }
 
-case class SIFTermCondNotLow(offendingNode: SIFTerminatesExp) extends AbstractErrorReason {
+case class SIFTermCondNotLow(offendingNode: SIFTerminatesExp) extends ExtensionAbstractErrorReason {
   val id: String = "sif_termination.condition_not_low"
   val readableMessage: String = s"Termination condition ${offendingNode.cond} might not be low."
 
@@ -45,7 +45,7 @@ case class SIFTermCondNotLow(offendingNode: SIFTerminatesExp) extends AbstractEr
     SIFTermCondNotLow(offendingNode.asInstanceOf[SIFTerminatesExp])
 }
 
-case class SIFTermCondLowEvent(offendingNode: SIFTerminatesExp) extends AbstractErrorReason {
+case class SIFTermCondLowEvent(offendingNode: SIFTerminatesExp) extends ExtensionAbstractErrorReason {
   val id: String = "sif_termination.not_lowevent"
   val readableMessage: String =
     s"Termination condition ${offendingNode.cond} evaluating to false might not imply both executions don't terminate."
@@ -54,7 +54,7 @@ case class SIFTermCondLowEvent(offendingNode: SIFTerminatesExp) extends Abstract
     SIFTermCondLowEvent(offendingNode.asInstanceOf[SIFTerminatesExp])
 }
 
-case class SIFTermCondNotTight(offendingNode: SIFTerminatesExp) extends AbstractErrorReason {
+case class SIFTermCondNotTight(offendingNode: SIFTerminatesExp) extends ExtensionAbstractErrorReason {
   val id: String = "sif_termination.condition_not_tight"
   val readableMessage: String = s"Termination condition ${offendingNode.cond} might not be tight."
 
diff --git a/src/main/scala/viper/gobra/translator/transformers/hyper/SIFLowGuardTransformer.scala b/src/main/scala/viper/gobra/translator/transformers/hyper/SIFLowGuardTransformer.scala
index 48efe3f1c..a13ed7455 100644
--- a/src/main/scala/viper/gobra/translator/transformers/hyper/SIFLowGuardTransformer.scala
+++ b/src/main/scala/viper/gobra/translator/transformers/hyper/SIFLowGuardTransformer.scala
@@ -131,11 +131,32 @@ trait SIFLowGuardTransformer {
     f.copy(name = ctx.rename(f.name))(f.pos, f.info, f.errT)
   }
 
-  def domain(d: Domain, @unused ctx: Context): Vector[Member] = Vector(d)
+  def domain(d: Domain, ctx: Context): Vector[Member] = {
+    val relationalTriggers = d.functions.filter(f => isRelationalTrigger(f.name)).map { f =>
+      val formalArgs = f.formalArgs.zipWithIndex.map{
+        case (v: LocalVarDecl, _) => v
+        case (v: UnnamedLocalVarDecl, idx) => LocalVarDecl(s"""v$idx""", v.typ)(v.pos, v.info, v.errT)
+      }
+
+      val newFormalArgs = formalArgs.map(runLocalVarDecl(_, ctx.major)) ++ formalArgs.map(runLocalVarDecl(_, ctx.minor))
+      DomainFunc(ctx.predicateFunctionName(f.name), newFormalArgs, Bool)(f.pos,f.info,d.name,f.errT)
+    }
+
+    val relationalAxioms = d.axioms.filter(ax => isRelational(ax.exp, ctx)).map {
+      case ax: NamedDomainAxiom => ax.copy(exp = assertion(ax.exp, ctx))(ax.pos, ax.info, ax.domainName, ax.errT)
+      case ax: AnonymousDomainAxiom => ax.copy(exp = assertion(ax.exp, ctx))(ax.pos, ax.info, ax.domainName, ax.errT)
+    }
+
+    Vector(d.copy(
+      functions = d.functions ++ relationalTriggers,
+      axioms = d.axioms ++ relationalAxioms,
+    )(d.pos,d.info,d.errT))
+  }
 
   def directlyRelational(e: Exp): Boolean = {
     e.exists {
       case _: SIFLowExp => true
+      case f: DomainFuncApp => isRelationalTrigger(f.funcname)
       case _ => false
     }
   }
@@ -143,6 +164,7 @@ trait SIFLowGuardTransformer {
   def isRelational(e: Exp, ctx: Context): Boolean = {
     e.exists {
       case _: SIFLowExp => true
+      case f: DomainFuncApp => isRelationalTrigger(f.funcname)
       case p: PredicateAccess => ctx.isRelationalPredicate(p.predicateName)
       case _ => false
     }
@@ -184,6 +206,13 @@ trait SIFLowGuardTransformer {
         case l: SIFLowExp => comparison(l, ctx)
         case l: SIFLowEventExp => TrueLit()(l.pos, l.info, l.errT)
 
+        case a: DomainFuncApp =>
+          assert(isRelationalTrigger(a.funcname), s"Expected relational trigger, but got $a.")
+          a.copy(
+            funcname = ctx.predicateFunctionName(a.funcname),
+            args = a.args.map(runExp(_, ctx.major)) ++ a.args.map(runExp(_, ctx.minor)),
+          )(a.pos, a.info, a.typ, a.domainName, a.errT)
+
         case p: PredicateAccess =>
           assert(isPositive)
           And(positiveUnary(p), predicateAccess(p.predicateName, p.args, ctx)(p.pos, p.info, p.errT))(p.pos, p.info, p.errT)
@@ -194,8 +223,7 @@ trait SIFLowGuardTransformer {
         case f: Forall =>
           Forall(
             variables = f.variables.map(runLocalVarDecl(_, ctx.major)) ++ f.variables.map(runLocalVarDecl(_, ctx.minor)),
-            triggers = f.triggers.map(t => Trigger(t.exps.map(runExp(_, ctx.major)))(t.pos, t.info, t.errT)) ++
-              f.triggers.map(t => Trigger(t.exps.map(runExp(_, ctx.minor)))(t.pos, t.info, t.errT)),
+            triggers = f.triggers.flatMap(trigger(_, ctx)),
             exp = go(f.exp, isPositive),
           )(f.pos, f.info, f.errT).autoTrigger
 
@@ -217,7 +245,13 @@ trait SIFLowGuardTransformer {
     Simplifier.simplify(go(e, isPositive = true))
   }
 
-
+  def trigger(t: Trigger, ctx: Context): Vector[Trigger] = {
+    def triggerExp(e: Exp): Vector[Exp] = {
+      if (isRelational(e, ctx)) Vector(assertion(e, ctx))
+      else Vector(runExp(e, ctx.major), runExp(e, ctx.minor))
+    }
+    Vector(Trigger(t.exps.flatMap(triggerExp))(t.pos,t.info,t.errT))
+  }
 
   def predicateAccess(p: String, args: Seq[Exp], ctx: Context)(pos: Position, info: Info, errT: ErrorTrafo): FuncApp = {
     FuncApp(
@@ -450,6 +484,8 @@ trait SIFLowGuardTransformer {
     case s: Seqn => s
     case s => Seqn(Seq(s), Seq.empty)(s.pos, s.info, s.errT)
   }
+
+  def isRelationalTrigger(s: String): Boolean = s.startsWith("rel_")
 }
 
 trait Context {