Consider the binary variables $x_1, x_2 \in \{0,1\}$ and the integer variable $y \in \mathbb{Z}$ with $0 \leq y \leq 3$.
I'd like to formulate the following logical constraint:
$$ x_1 = 1 \wedge y \geq 2 \implies x_2 = 1 $$
and I don't have access to commercial solvers or modelling frameworks. Any ideas?