sat_max_maxundef_all_with_tempinduct_fail.pat 95 Bytes