Draft: MR for code review of branch interpolation-model-checking

This branch includes the following updates:

• Implement witness generation for IMC and ISMC Algorithms (experimental results)

Merge request for code review and discussions only, merge must be done with svn merge.