source: CIVL/examples/languageFeatures/choose.cvl

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

int n = 2;
float x;

void main() {
l1:
  $choose {
    $when (n>2) { x=2; goto l2; }
    $when (n>1) { x=1; goto l2; }
    default: {x=0; goto l2; }
  }
l2: ;
$choose {
        { x == 0; }
        x == 1;
        $when(x < 0) x == 2;
        }
}