# How to write operational semantics rule for havoc x?

If I want to extend a new language by adding a new command havoc x, which updates the variable x with a non-deterministic value, how to write operational semantics rule for havoc x? I'm confused about generate a non-deterministic value. If I write like this: $$\frac{n = [e]_ {intexp}\sigma}{(\mathrm{havoc}\ x,\sigma)\rightarrow(x:=x+n,\sigma)}$$ is it make sense?

I'm going to assume that all the allowed values for $x$ are (unbounded) integers.
In that case your proposal somewhat makes sense, insomuch as $e$ is some arbitrary well-formed expression (which evaluates to some value in the context $\sigma$). But it's just as easy to write this
$$\frac{n\in\mathbb{Z}}{(\mathrm{havoc}\ x,\sigma)\rightarrow (x:=n,\sigma)}$$
You see that in both cases the result of the evaluation by this rule can non-deterministically give any value in $\mathbb{Z}$ to $x$. In this sense, you have a family of rules, one for each $n\in\mathbb{Z}$.