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 }        
  }