Updating test annotations for Z3 4.16.0

src/test/resources/all/annotation/annotationProverConfigArgs.vpr

@@ -42,11 +42,11 @@ method m1(i: Int, i2: Int)
 
 @proverConfigArgs("smt.arith.nl=false")
 method m2(i: Int, i2: Int)
-    requires i >= 0
-    requires i2 >= 0
+    requires i >= 2
+    requires i2 >= 2
 {
     //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/000/)
-    assert i * i2 >= 0
+    assert i * i2 >= 4
 }
 
 @proverConfigArgs("smt.arith.nl=true")

src/test/resources/all/basic/quantifiers.vpr

@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field Cell_x: Int
 
 function Cell_get(this: Ref): Int
@@ -117,11 +117,11 @@ method test1(A: Seq[Int]) {
 	assume forall v1: Int ::
 		(0 <= v1 && v1 < 3 && f2(v1)) ==> (exists j1: Int :: 0 <= j1 && j1 < 3 && j1 == v1)
 
-  //:: ExpectedOutput(assert.failed:assertion.false)
 	assert forall v2: Int ::
 		(0 <= v2 && v2 < 3 && f2(v2)) ==> (exists j2: Int :: 0 <= j2 && j2 < 3 && j2 == v2)
     /* 2013-08-05 Malte: Fails, probably due to a triggering problem of Z3.
      *            Should hold otherwise.
+     * 2026 Marco: Fails in Z3 4.8.7, passes in 4.16.0.
      */
 }
 

src/test/resources/all/issues/carbon/0073.vpr

@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field data: Int
 field rds: Int
 
@@ -11,7 +11,6 @@ method test(this: Ref, I: Perm)
   exhale acc(this.data, write)
   assert this.rds >= 0
   //assert I > none   // Uncommenting this makes a program to verify.
-  //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/73/) 
-  // check Z3 version - this seems to work with some versions
+  // did not verify in 4.8.7, verifies in 4.16.0
   assert this.rds * I > none
 }

src/test/resources/all/issues/carbon/0202.vpr

@@ -32,8 +32,7 @@ method qpTest(a: Array, j:Int)
 {
   assume dummy(j-2)
   loc(a,j).val := 5
-  //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/202/)
-  assert exists k:Int :: dummy(k-2) && 0 <= k 
+  assert exists k:Int :: dummy(k-2) && 0 <= k
 }
 
 domain test{

src/test/resources/all/issues/silicon/0005a.vpr

@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 function trigF(x: Int, y: Int): Bool
   requires acc(P())
 { true }
@@ -16,6 +16,7 @@ method test(flag: Bool)
   requires forall a: Int, b: Int :: true ==> trigG(a, flag) && trigF(a, b)
   ensures  acc(P())
   //:: UnexpectedOutput(postcondition.violated:assertion.false, /carbon/issue/39/)
+  //:: UnexpectedOutput(postcondition.violated:assertion.false, /silicon/issue/5/)
   ensures forall a: Int, b: Int :: true ==> trigG(a, flag) && trigF(a, b)
 {}
 

src/test/resources/all/issues/silicon/0183.vpr

@@ -16,16 +16,12 @@ method foo_ok(self: Ref)
 method foo_fail(self: Ref, rd: Perm)
   requires none < rd && rd < write
   requires acc(valid__Cell(self, rd), rd)
-  //:: UnexpectedOutput(not.wellformed:insufficient.permission, /Silicon/issue/183/)
-  //:: UnexpectedOutput(not.wellformed:insufficient.permission, /Carbon/issue/83/)
   requires (unfolding acc(valid__Cell(self, rd), rd) in self.v) == 1
 {}
 
 method foo_fail_gist(self: Ref, rd: Perm)
   requires none < rd && rd < write
 {
-  //:: UnexpectedOutput(assert.failed:assertion.false, /Silicon/issue/183/)
-  //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/83/)
   assert none < rd * rd
 }
 
@@ -34,16 +30,12 @@ method bar(self: Ref, rd: Perm)
   requires acc(valid__Cell(self, rd), rd)
 {
   unfold acc(valid__Cell(self, rd), rd)
-  //:: UnexpectedOutput(assert.failed:insufficient.permission, /Silicon/issue/183/)
-  //:: UnexpectedOutput(assert.failed:insufficient.permission, /Carbon/issue/83/)
   assert self.v >= self.v
 }
 
 method bar_gist(self: Ref, rd: Perm)
   requires none < rd && rd < write
 {
-  //:: UnexpectedOutput(assert.failed:assertion.false, /Silicon/issue/183/)
-  //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/83/)
   assert none < rd * rd
 }
 

src/test/resources/all/issues/silicon/0302.vpr

@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 domain Array {
 
   function loc(a: Array, i: Int): Ref
@@ -34,6 +34,7 @@ method testspec_skipping_indices1(arr: Array, size: Int, rdAmount: Perm)
     assert forall j:Int :: acc(loc(arr,j).val, (j < 0 || j >= size ? none : (j % 2 == 0 ? rdAmount : write)))
     assert forall j:Int :: (j < 0 || j >= size ? none : (j % 2 == 0 ? rdAmount : write)) <= p(j, size, rdAmount)
     assert forall j:Int :: (j < 0 || j >= size ? none : (j % 2 == 0 ? rdAmount : write)) >= p(j, size, rdAmount)
+    //:: UnexpectedOutput(assert.failed:insufficient.permission, /carbon/issue/585/)
     assert forall j:Int :: acc(loc(arr,j).val, (j < 0 || j >= size ? none : write)) // should fail, and does 
   }
 
@@ -46,5 +47,6 @@ method testspec_skipping_indices2(arr: Array, size: Int, rdAmount: Perm)
     assert forall j:Int :: (j < 0 || j >= size ? none : (j % 2 == 0 ? rdAmount : write)) <= p(j, size, rdAmount)
     assert forall j:Int :: (j < 0 || j >= size ? none : (j % 2 == 0 ? rdAmount : write)) >= p(j, size, rdAmount)
     //:: ExpectedOutput(assert.failed:insufficient.permission)
+    //:: MissingOutput(assert.failed:insufficient.permission, /carbon/issue/585/)
     assert forall j:Int :: acc(loc(arr,j).val, (j < 0 || j >= size ? none : write)) // should fail, and does 
   }

src/test/resources/all/issues/silicon/0508a.vpr

@@ -25,7 +25,6 @@ method test03b(trees: Set[Ref])
 {
   //:: ExpectedOutput(assert.failed:qp.not.injective)
   //:: ExpectedOutput(assert.failed:insufficient.permission)
-  //:: MissingOutput(assert.failed:qp.not.injective, /carbon/issue/361/)
   //:: MissingOutput(assert.failed:insufficient.permission, /silicon/issue/34/)
   assert forall s: Ref :: {id(s)} s in trees ==> acc(id(s).item.bool_prop, wildcard)
 }

src/test/resources/all/issues/silicon/0695.vpr

@@ -73,6 +73,7 @@ method foo(x: Ref, lft: Map[Int, Map[Ref, Perm]]) returns (res: Ref, new_lft: Ma
     //:: ExpectedOutput(fold.failed:insufficient.permission)
     fold LifetimeP(new_lft)
 
+    //:: UnexpectedOutput(fold.failed:insufficient.permission, /carbon/issue/585/)
     fold acc(lft_List(x_nxt), new_lft[tpListT][x.ref])
 
     new_lft := new_lft

src/test/resources/all/issues/silver/0522.vpr

@@ -58,6 +58,7 @@ method test21(xs: Set[Ref], p: Perm) {
     //:: ExpectedOutput(invariant.not.established:negative.permission)
     //:: MissingOutput(invariant.not.established:negative.permission, /Silicon/issue/34/)
     //:: ExpectedOutput(not.wellformed:negative.permission)
+    //:: UnexpectedOutput(invariant.not.preserved:negative.permission, /carbon/issue/585/)
     invariant forall x: Ref :: x in xs ==> acc(P(x), p)
   {}
 }

src/test/resources/all/permission_introspection/forpermPredicatesAdvanced.vpr

@@ -16,7 +16,6 @@ method m2(x: Ref, y: Ref, z: Ref) {
     inhale p2(z, y)
     inhale x != z
 
-    //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/243/)
     assert !forperm a: Ref [p2(a,y)] :: a == z
     unfold p2(x,y)
     assert forperm a: Ref [p2(a,y)] :: a == z

src/test/resources/all/permission_introspection/forpermQP.vpr

@@ -14,7 +14,6 @@ field f: Int
        inhale acc(g.f)
        inhale forall a: Ref :: a == g ==> acc(a.f) && a.f < 3
 
-       //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/243/)
        assert !forperm a: Ref [a.f] :: a.f > 3
 
        inhale forall a: Ref :: a == x || a == y ==> a.f == 4

src/test/resources/counterexample_general/qpred.vpr

@@ -17,6 +17,8 @@ method foo(refs: Set[Ref], r2: Ref, r3: Ref, rp: Ref, ip: Int)
     assert P(r3, 3);
     exhale acc(P(r2, 4), 1/2)
 
+    assert acc(P(r3, 3), 1/1)
+
     //:: ExpectedCounterexample(assert.failed:insufficient.permission, (acc(P(r3, 3), 1/1), acc(P(r2, 4), 1/2)))
     assert acc(P(rp, ip))
   }

src/test/resources/examples/vmcai2016/linked-list-predicates.vpr

@@ -2,6 +2,7 @@
 // http://creativecommons.org/publicdomain/zero/1.0/
 
 //:: IgnoreFile(/carbon/issue/280/)
+//:: IgnoreFile(/silicon/issue/1004/)
 
 /*****************************************************************
  * List Nodes
@@ -22,7 +23,7 @@ function contentNodes(this: Ref, end: Ref): Seq[Int]
   ensures  this == end ==> result == Seq[Int]()
   ensures  this != end ==>
               0 < |result| && result[0] == unfolding acc(lseg(this, end)) in this.data
-  ensures  forall i: Int, j: Int :: 0 <= i && i < j && j < |result| ==> result[i] <= result[j]
+  ensures  forall i: Int, j: Int ::  { result[i], result[j] } 0 <= i && i < j && j < |result| ==> result[i] <= result[j]
 {
   this == end ? Seq[Int]() :
                 unfolding acc(lseg(this, end)) in (
@@ -54,7 +55,7 @@ predicate List(this: Ref)
 
 function content(this: Ref): Seq[Int]
   requires acc(List(this))
-  ensures  forall i: Int, j: Int :: 0 <= i && i < j && j < |result| ==> result[i] <= result[j]
+  ensures  forall i: Int, j: Int :: { result[i], result[j] } 0 <= i && i < j && j < |result| ==> result[i] <= result[j]
 {
   unfolding acc(List(this)) in contentNodes(this.head, null)
 }
@@ -134,9 +135,9 @@ method insert(this: Ref, elem: Int) returns (index: Int)
       invariant acc(ptr.next) && acc(ptr.data) && ptr.data <= elem
       invariant acc(lseg(ptr.next, null))
       invariant acc(lseg(this.head, ptr))
-      invariant forall i: Int :: 0 <= i && i < |contentNodes(this.head, ptr)| ==>
+      invariant forall i: Int :: { contentNodes(this.head, ptr)[i] } 0 <= i && i < |contentNodes(this.head, ptr)| ==>
                   contentNodes(this.head, ptr)[i] <= ptr.data
-      invariant forall i: Int :: 0 <= i && i < |contentNodes(ptr.next, null)| ==>
+      invariant forall i: Int :: { contentNodes(ptr.next, null)[i] } 0 <= i && i < |contentNodes(ptr.next, null)| ==>
                   ptr.data <= contentNodes(ptr.next, null)[i]
       invariant index-1 == |contentNodes(this.head, ptr)|
       invariant

src/test/resources/quantifiedpermissions/sequences/bsearch.vpr

@@ -7,9 +7,9 @@ field f: Int
 
 method bfind_orig(S: Seq[Ref], x: Int, p: Perm) returns (index: Int)
   requires p > none && p < write
-  requires forall i: Int, j: Int :: i in [0..|S|) && j in [0..|S|) && i != j ==> S[i] != S[j]
+  requires forall i: Int, j: Int :: { S[i], S[j] } i in [0..|S|) && j in [0..|S|) && i != j ==> S[i] != S[j]
   requires forall i: Int :: {S[i].f} i in [0..|S|)  ==> acc(S[i].f, p)
-  requires forall i: Int :: {S[i].f} i in [0..|S|-1)  ==> S[i].f < S[i + 1].f
+  requires forall i: Int, j: Int :: {S[i].f, S[j].f} i < j && i in [0..|S|) && j in [0..|S|) ==> S[i].f < S[j].f
   ensures forall i: Int :: {S[i].f} i in [0..|S|) ==> acc(S[i].f, p)
   ensures index in [-1..|S|)
   //:: ExpectedOutput(postcondition.violated:assertion.false)

src/test/resources/quantifiedpermissions/sequences/linked-list-qp-append.vpr

@@ -13,10 +13,10 @@ field data: Seq[Int]
 predicate List(this: Ref)
 {
 	acc(this.nodes)
-   && (forall i: Int, j: Int :: i in [0..|this.nodes|) && j in [0..|this.nodes|) && i != j ==> this.nodes[i] != this.nodes[j])
-   && (forall i: Int :: 0 <= i && i < |this.nodes| ==> acc(this.nodes[i].val))
-	 && (forall i: Int :: 0 <= i && i < |this.nodes| ==> acc(this.nodes[i].next))
-	 && (forall i: Int :: {this.nodes[i].next} (0 <= i && i < |this.nodes| ==>
+   && (forall i: Int, j: Int :: { this.nodes[i], this.nodes[j] } i in [0..|this.nodes|) && j in [0..|this.nodes|) && i != j ==> this.nodes[i] != this.nodes[j])
+   && (forall i: Int :: { this.nodes[i] } 0 <= i && i < |this.nodes| ==> acc(this.nodes[i].val))
+	 && (forall i: Int :: { this.nodes[i] } 0 <= i && i < |this.nodes| ==> acc(this.nodes[i].next))
+	 && (forall i: Int :: { this.nodes[i].next } (0 <= i && i < |this.nodes| ==>
 	 	    this.nodes[i] in this.nodes && (i < |this.nodes| - 1 ? this.nodes[i].next == this.nodes[i+1] : this.nodes[i].next == null)
 	 ))
 }
@@ -40,13 +40,13 @@ method append(this: Ref, elem: Int)
   ensures acc(List(this))
   ensures length(this) == old(length(this)) + 1
   ensures itemAt(this, length(this) - 1) == elem
-  ensures forall i: Int :: 0 <= i && i < length(this) - 1 ==> itemAt(this, i) == old(itemAt(this, i))
+  ensures forall i: Int :: { itemAt(this, i) } 0 <= i && i < length(this) - 1 ==> itemAt(this, i) == old(itemAt(this, i))
 {
 	unfold acc(List(this))
 
  	var n : Ref
 	n := new()
-	inhale acc(n.val) && acc(n.next) && (forall i: Int :: (0<=i && i < |this.nodes|) ==> this.nodes[i] != n)
+	inhale acc(n.val) && acc(n.next) && (forall i: Int :: { this.nodes[i] } (0<=i && i < |this.nodes|) ==> this.nodes[i] != n)
 
 	n.next := null
 	n.val := elem

src/test/resources/quantifiedpermissions/third_party/testZeroSubmatrix.vpr

@@ -1,6 +1,8 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
+//:: IgnoreFile(/carbon/issue/93/)
+
 field Ref__Integer_value: Int
 
 function Ref__multidim_index_2(N0: Int, N1: Int, i0: Int, i1: Int): Int