Update regression test for 'ignore-safety'.

This tracks changes to the symbolic indexing primitives.
GaloisInc · Jul 26, 2021 · 664c857 · 664c857
1 parent c533996
commit 664c857
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.