Great! :-)

Merged and pushed.

OK, feel free to merge if you like.

Well, we had to expect that there would be cases where the algorithms perform 
better and cases where they perform worse. The only notable change I see is 
that the original M&S mas-buckets config solves 3 tasks in barman, whereas it 
solves no task with the new RNG. I looked into the logs and it seems that the 
reason is that with the new "shrink order" there's not enough memory to merge 
all variables. I don't know if we can or should do anything about this.

Thanks! What do you make of the data?

As suggested I ran two experiments, here are the results:

http://ai.cs.unibas.ch/_tmp_files/seipp/issue269-opt-issue269-base-issue269-v1-
compare.html
http://ai.cs.unibas.ch/_tmp_files/seipp/issue269-sat-issue269-base-issue269-v1-
compare.html

So, I did add some more comments after all, but now I'm done.

To clarify, what I meant was: it would be good to address the comment about
shuffling in particular first because it might affect the interface of g_rng
(which would need to become compatible with the standard library's URNGs). This
is a large enough change that I think it would be good to rereview afterwards,
so I'd rather review the rest of the changes then rather than doing it twice.

I've made two initial comments and would suggest rereviewing later.

I made a pull request at bitbucket. Can you have a look at the code, please?

The new RNG should be used everywhere. Search for srand, rand, random_shuffle.