$input int B;
$input int N;
$assume 0<N && N<B;
int n = 3;

void main(){
	int x;
	
	$atomic{
		x = N;
		x = x * 2;
	}
	$assert x == 2*N;
	// non-determinism allowed in $atomic block
	$atomic{
		x = 3;
		$choose {
			$when (n>2) { x=2;  }
			$when (n>1) { x=1;  }
			default: {x=0;  }
		}
	}
	$assert (x == 2 || x == 1);
}