Slightly extended test to cover a case that needs an adjustment in Silicon

Author: marcoeilers

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

@@ -4,12 +4,23 @@
 method main() {
     assume forall qvar: Int ::
       let alias == (qvar) in
-        f_get(alias) == f_clamp() 
+        f_get(alias) == f_clamp()
     assert f_get(10) == 0
 }
 
 function f_get(idx: Int): Int
 
 
+method main2() {
+    assume forall qvar: Int :: qvar > 0 ==>
+      let alias == (qvar) in
+        f_get2(alias) == f_clamp()
+    assert f_get2(10) == 0
+}
+
+function f_get2(idx: Int): Int
+    requires idx > -5
+
+
 function f_clamp(): Int
   ensures result == 0