From 142d5d7467a5d88452800071ad4384971f0cf9b7 Mon Sep 17 00:00:00 2001
From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com>
Date: Wed, 20 Mar 2024 15:58:28 +0100
Subject: [PATCH] Remove bad trigger

Keeping this trigger causes profiling to fail, as the trigger cannot be found in the body of the quantifier.
---
 dicts/dicts.gobra | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dicts/dicts.gobra b/dicts/dicts.gobra
index ddbb3bb..bcbf125 100644
--- a/dicts/dicts.gobra
+++ b/dicts/dicts.gobra
@@ -147,7 +147,7 @@ ghost
 opaque
 decreases
 pure func IsTotal(d dict[int]int) bool {
-	return forall k int :: {d[k]} {k in domain(d)} k in domain(d)
+	return forall k int :: {k in domain(d)} k in domain(d)
 }
 
 // True iff a dictionary is monotonic.