unrelacy: use new MODEL_ASSERT() macro