let th_of_string s = Th.to_int (Th.of_string s)