$input int a[10]; $assume($forall (int i : 0 .. 9) a[i] == 0); int proc(int i) { if (i == 0) $when(*(a+9) == 0) return 0; else $when(*(a+9) == 0 && *(a+10) == 0) return 1; // guard with error side effect will evaluate to false } int main() { $parfor(int i : 0 .. 1) proc(i); return 0; }