Michal Hrusecky authored Mar 16, 2020 and Karel Koci committed Mar 16, 2020

This enables pseudorandom generator and dynamic variable "$RANDOM". It
will be quite useful and we wouldn't need to come with something crazy.