/* Commandline execution:
 *		civl verify switch.cvl
 * */
#include <civlc.cvh>
$input int i;
$assume(i >= 0 && i < 10);

void main() {
  switch (i) {
    case 0:
      $assert(i == 0);
      break;
    case 1:
    case 2:
    case 3:
      $assert(i < 4);
      break;
    default:
      $assert(i > 3);
  }
}