adds injectivity to 2 test cases

src/test/resources/regressions/features/make_and_new/make1.gobra

@@ -27,8 +27,10 @@ func accessOutsideLen() {
 }
 
 requires length > 0 && capacity >= length
-ensures forall i int :: (0 <= i && i < length) ==> acc(&ret[i]) && ret[i] == 0
+// note that the postconditions must occur in the following order. Otherwise, `length` is not constraint to `len(ret)` in
+// the forall quantifier. In this case, `ret[i]` is not known to be injective.
 ensures len(ret) == length && cap(ret) == capacity
+ensures forall i int :: (0 <= i && i < length) ==> acc(&ret[i]) && ret[i] == 0
 func Ok1(length int, capacity int) (ret []int) {
 	ret := make([]int, length, capacity)
 }

src/test/resources/regressions/features/slices/slice-index-fail2.gobra

@@ -9,11 +9,13 @@ func foo(s []int) {
   n := s[0]
 }
 
-requires forall i int :: 0 <= i && i < len(s) ==> acc(&s[i]) && acc(s[i])
+requires forall i int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i])
+requires forall i, j int :: { s[i], s[j] } 0 <= i && i < j && j < len(s) ==> s[i] != s[j] // injectivity
+requires forall i int :: { s[i] } 0 <= i && i < len(s) ==> acc(s[i])
 func bar(s []*int)
 
 func barRun() {
   s := make([]*int, 2)
-  //:: ExpectedOutput(precondition_error:receiver_not_injective)
+  //:: ExpectedOutput(precondition_error:assertion_error)
   bar(s)
-}
+}