Z3で疑似乱数生成器(xorshift)の出力を予測する

1年以上昔にこんな記事を書いた。 burion.net 久しぶりに読み返してみると、疑似乱数が決定的・周期的なことまではなんとなく示せているものの具体的な予測方法は全然書いてないじゃん!!!と内なる声に突っ込まれた。「予測できるか試したい」なんてタイトル掲げておいて、なんて中途半端な奴なんだ。 多分このときは周…