KLEE_RUN_TEST_ERROR: object name mismatch. Requesting “output_port” but returning “user_buf”

I recently has a project to do with using replay ktests with KLEE.