/* 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);
  $assert($exists (int k: 0 .. 4) 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);
}