Termination checks are enabled (see termination.fst for some examples); all other existing unit tests all proven with termination checks