/* Commandline execution:
 *		civl verify quantifiers.cvl
 * */
#include<civlc.cvh>

$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));
}