Test for Carbon issue #391 (#829)

Author: marcoeilers

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

@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+predicate p()
+
+method mmmm()
+{
+ //:: ExpectedOutput(exhale.failed:qp.not.injective)
+ //:: ExpectedOutput(exhale.failed:insufficient.permission)
+ //:: MissingOutput(exhale.failed:insufficient.permission, /silicon/issue/34/)
+ exhale forall i: Int :: p()
+}
+
+method mmmm2()
+{
+ //:: ExpectedOutput(inhale.failed:qp.not.injective)
+ inhale forall i: Int :: p()
+}

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

@@ -7,7 +7,6 @@ predicate P()
 
 method test()
   requires P()
-   //:: IgnoreFile(/carbon/issue/391/)
   ensures forall i: Int :: i == 0 ==> P()
 {}