#include<civlc.h>
$input double b[10];

void main() {
  int a[5];
  
  for (int i = 0; i < 5; i++) {
    a[i] = i;
  }
  $assert $forall {int i | i >= 0 && i < 5} a[i] >= 0;
  $assert $exists {int k | k >= 0 && k < 5} a[k] > 3;
  $assume $forall {int j | j >= 0 && j < 10} b[j] >= 2;
  $assert $forall {int m | m >= 3 && m <= 5} b[m] > 1;
}