Joris Kinable - 2019-03-31

Oddly, substituting this:

0/"$r$"; 
13/"$t$";
2/"$u_{2}$";
3/"$u_{3}$";
4/"$u_{4}$";
5/"$u_{5}$";
6/"$u_{6}$";
7/"$u_{7}$";
8/"$u_{8}$";
9/"$u_{9}$";
10/"$u_{10}$";
11/"$u_{11}$";
12/"$u_{12}$";

by this (i.e. simply reordering) also fixes the problem:

0/"$r$"; 
2/"$u_{2}$";
3/"$u_{3}$";
4/"$u_{4}$";
5/"$u_{5}$";
6/"$u_{6}$";
7/"$u_{7}$";
8/"$u_{8}$";
9/"$u_{9}$";
10/"$u_{10}$";
11/"$u_{11}$";
12/"$u_{12}$";
13/"$t$";