Removed no longer necessary assertion from test case

viperproject · May 20, 2022 · 5503e4a · 5503e4a
1 parent 8186861
commit 5503e4a
Showing 1 changed file with 27 additions and 28 deletions.
diff --git a/src/test/resources/all/issues/silicon/0285.vpr b/src/test/resources/all/issues/silicon/0285.vpr
@@ -22,31 +22,30 @@ field val : Int
   method havocArray() returns (a:Array)
   method havocInt() returns (i:Int)
 
-  method setToArray(vals:Set[Int]) returns (a:Array)
-    ensures len(a) == |vals|
-    ensures forall i:Int :: 0 <= i && i< len(a) ==> acc(loc(a,i).val)
-    ensures forall i:Int :: i in vals ==> exists k: Int :: 0 <= k && k < len(a) && loc(a,k).val == i
-    {
-      // model allocating an array of size |vals|
-      a := havocArray()
-      assume len(a) == |vals|
-      inhale forall i:Int :: 0 <= i && i< len(a) ==> acc(loc(a,i).val)
-
-      var s : Set[Int] := vals
-      var element : Int; var j : Int := 0;
-
-      while (|s| > 0)
-      invariant forall i:Int :: 0 <= i && i< len(a) ==> acc(loc(a,i).val)
-      invariant s subset vals
-      invariant j == |vals setminus s|
-      invariant forall i:Int :: {i in vals} i in (vals setminus s) ==> exists k: Int :: 0 <= k && k < j && loc(a,k).val == i
-      {
-        var t : Set[Int] := s
-        element := havocInt()
-        assume element in s // choose an element
-        loc(a,j).val := element
-        s := s setminus Set(element)
-        j := j + 1
-        assert vals setminus s == (vals setminus t) union Set(element) // or add {i in vals} trigger to loop invariant
-      }
-    }
+method setToArray(vals:Set[Int]) returns (a:Array)
+  ensures len(a) == |vals|
+  ensures forall i:Int :: 0 <= i && i< len(a) ==> acc(loc(a,i).val)
+  ensures forall i:Int :: i in vals ==> exists k: Int :: 0 <= k && k < len(a) && loc(a,k).val == i
+{
+  // model allocating an array of size |vals|
+  a := havocArray()
+  assume len(a) == |vals|
+  inhale forall i:Int :: 0 <= i && i< len(a) ==> acc(loc(a,i).val)
+
+  var s : Set[Int] := vals
+  var element : Int; var j : Int := 0;
+
+  while (|s| > 0)
+  invariant forall i:Int :: 0 <= i && i< len(a) ==> acc(loc(a,i).val)
+  invariant s subset vals
+  invariant j == |vals setminus s|
+  invariant forall i:Int :: {i in vals} i in (vals setminus s) ==> exists k: Int :: 0 <= k && k < j && loc(a,k).val == i
+  {
+    var t : Set[Int] := s
+    element := havocInt()
+    assume element in s // choose an element
+    loc(a,j).val := element
+    s := s setminus Set(element)
+    j := j + 1
+  }
+}