adapts regression tests to latest Viper changes

koflin · Jul 3, 2023 · d64f56a · d64f56a
1 parent 9772277
commit d64f56a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/src/test/resources/regressions/features/closures/closures-calldesc2.gobra b/src/test/resources/regressions/features/closures/closures-calldesc2.gobra
@@ -33,6 +33,7 @@ func hof(ghost cs Calls, f func(ghost seq[int], int)int)(res int) {
 
 ghost
 ensures forall k int :: k > 0 && len(s) == k ==> res == s[k-1] + seqSum(s[:(k-1)])
+decreases len(s)
 pure func seqSum(s seq[int]) (res int) {
     return len(s) == 0 ? 0 : (s[len(s)-1] + seqSum(s[:(len(s)-1)]))
 }

diff --git a/src/test/resources/regressions/features/closures/closures-calldesc4-map.gobra b/src/test/resources/regressions/features/closures/closures-calldesc4-map.gobra
@@ -112,6 +112,7 @@ func test2() {
 
 ghost
 ensures forall k int :: k > 0 && len(s) == k ==> res == s[k-1] + seqSum(s[:(k-1)])
+decreases len(s)
 pure func seqSum(s seq[int]) (res int) {
     return len(s) == 0 ? 0 : (s[len(s)-1] + seqSum(s[:(len(s)-1)]))
 }