agra-uni-bremen/metaSMT — pull request #4 by hpalikareva (2013-08-07 12:29:18+00:00)
Title: Added support for using the QF_ABV fragment in the STP backend

Dear metaSMT team,

I have been trying to add support in KLEE for using a number of SMT solvers via metaSMT. Cristian Cadar and I had a paper about that at CAV 2013 (http://srg.doc.ic.ac.uk/publications/klee-multisolver-cav-13.html), and I am now integrating the code into mainline KLEE. I had once sent you this patch that enables reasoning about arrays in the STP backend, but now that we started using github as well, it would be much easier if I just issue a pull request. It would be great if you apply the patch because otherwise we would need to supply it separately somewhere and ask users to apply it manually after obtaining the latest version of metaSMT. Please let me know what you think about that and whether you would like any modifications of the patch.

Thank you and best regards,
Hristina