Update regression test for 'ignore-safety'.

This tracks changes to the symbolic indexing primitives.
GaloisInc · Aug 3, 2021 · 8e91fe5 · 8e91fe5
1 parent e54f8d9
commit 8e91fe5
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 4 deletions.
diff --git a/tests/regression/ignore-safe.icry b/tests/regression/ignore-safe.icry
@@ -10,7 +10,6 @@
 :prove (\ (x:[8]) y -> (y == 0) || (y*(x/y) + x%y == x))
 
 :prove (\ (x:Integer) -> [0,0,0]@x == 0 )
-:prove (\ (x:Integer) -> []@x == 0 )
 :prove (\ (x:[8]) -> [0,0,0]@x == 0 )
 
 :set ignore-safety = on
@@ -22,5 +21,4 @@
 :prove (\ (x:[8]) y -> (y == 0) || (y*(x/y) + x%y == x))
 
 :prove (\ (x:Integer) -> [0,0,0]@x == 0 )
-:prove (\ (x:Integer) -> []@x == 0 )
 :prove (\ (x:[8]) -> [0,0,0]@x == 0 )
diff --git a/tests/regression/ignore-safe.icry.stdout b/tests/regression/ignore-safe.icry.stdout
@@ -11,5 +11,3 @@ Q.E.D.
 Q.E.D.
 Q.E.D.
 Q.E.D.
-Q.E.D.
-Q.E.D.
-Original file line number
+Diff line change
@@ Expand Up / @@ -11,5 +11,3 @@ Q.E.D. @@
     Q.E.D.
     Q.E.D.
     Q.E.D.
-    Q.E.D.
-    Q.E.D.