Follow up work for executable trace

[celinval]

• [ ] Use ? to propagate the error up.
• [ ] Don't use return at the end of the function.
• [ ] Refactor parser::parse_results to stop using output parameters and use return value instead.
• [ ] Create an issue to support multiple harnesses. Add the issue to the warning message.
• [ ] Rename feature.
• [ ] Ensure executable trace cannot run with formula slice. Related to https://github.com/model-checking/kani/issues/1288

[sanjit-bhat]

Also refactor code to allow insertion of multiple unit tests.