Fix remaining trigger issue

viperproject · Mar 4, 2024 · 83c3aa7 · 83c3aa7
1 parent 81d515e
commit 83c3aa7
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/dicts/dicts.gobra b/dicts/dicts.gobra
@@ -182,7 +182,7 @@ ghost
 opaque
 decreases
 pure func IsEqualInRange(d1, d2 dict[int]int, start, end int) bool {
-	return forall k int :: {d1[k], d2[k]} (start <= k && k < end) ==>
+	return forall k int :: {d1[k], d2[k]} {k in domain(d1)} {k in domain(d2)}(start <= k && k < end) ==>
 		k in domain(d1) && k in domain(d2) && d1[k] == d2[k]
 }
 

diff --git a/gomap/gomap.gobra b/gomap/gomap.gobra
@@ -154,21 +154,19 @@ pure func IsMonotonicFromTo(m map[int]int, start, end int) (result bool) {
 ghost
 requires acc(m1, _)
 requires acc(m2, _)
-// QUES Does not verify
 ensures result == dicts.IsEqualInRange(ToDict(m1), ToDict(m2), start, end)
 opaque
 decreases
 pure func IsEqualInRange(m1, m2 map[int]int, start, end int) (result bool) {
 	return let _ := reveal dicts.IsEqualInRange(ToDict(m1), ToDict(m2), start, end) in
-	(forall k int :: {m1[k], m2[k]} (start <= k && k < end) ==>
+	(forall k int :: {m1[k], m2[k]} {k in domain(m1)} {k in domain(m2)} (start <= k && k < end) ==>
 		k in domain(m1) && k in domain(m2) && m1[k] == m2[k])
 }
 
 // True iff m1 and m2 agree on all keys that their domains share.
 ghost
 requires acc(m1, _)
 requires acc(m2, _)
-// QUES Does not verify
 ensures result == dicts.Agree(ToDict(m1), ToDict(m2))
 decreases
 pure func Agree(m1, m2 map[int]int) (result bool) {