still some infinite loop on some unrollings (eg. pldi/InsertionSort:min), but some examples are solved. yay.