You are right, but I wrote it this way because I want to extend it in the near future. For instance, the run() method will call search, then it will filter the 'feasible' configurations (the equivalent of the feasible execution paths) using the SMT solver, and then it will choose one configuration (pseudo-randomly) from the feasible ones and continue the execution. The main reason is that I want to decouple the RewriteEngine from the SMT solver.

If you are not ok with this then I can simply inherit MaudeKRun, but again, this will change in the future.