Chalice/tests/regressions/workitem-10195.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

class Test { 
    method fails() 
    { 
      assert forall j in [10..5] :: true // ERROR: min > max
      assert false // failed previously, now we get a smoke warning
    }   
   
    method succeeds1() 
    { 
      assert forall j in [10..5] :: f(j) == 0 // ERROR: min > max
      assert false // failed previously, now we get a smoke warning
    } 
     
    method fails1() 
    { 
      assert forall j in [5..10] :: f(j) == 0
    }
        
        method succeeds2(a: int, b: int)
            requires 0 <= a && 0 <= b
            requires f(a) < f(b)
        {
      assert forall j in [f(b)..f(a)] :: f(j) == 0 // ERROR: min > max
            assert false // holds
        }
        
        method fails2(a: int, b: int)
            requires 0 <= a && 0 <= b
            requires 0 < f(a)
            requires f(a) < f(b)
        {
      assert forall j in [f(a)..f(b)] :: f(j) == 0
        }
     
    function f(i: int): int 
      requires 0 <= i
    { 0 }        
  }