turn_into_tuple(store, pn_Store_max);
set_Tuple_pred(store, pn_Store_M, store_mem);
set_Tuple_pred(store, pn_Store_X_except, new_Bad());
turn_into_tuple(store, pn_Store_max);
set_Tuple_pred(store, pn_Store_M, store_mem);
set_Tuple_pred(store, pn_Store_X_except, new_Bad());