ищу open source SMT solver/prover - замену проприетарщине от Microsoft Z3

Ничего не понял но

Coq (?)
на Haskell

agda

существует ли такая программа, но на Haskell

А зачем такое ограничение? В чем проблема использовать любой из тех, что на окамле?

В рамках проекта возникла задача использовать символьное выполнение (symbolic execution) некоторого псевдокода, получающегося из программы

А на каком языке написана исходная программа? Не может быть, что получится выкроить сразу весь модуль символьного вычисления из какого-нибудь SLAyer или JPF?

это не ограничение, это вторая часть вопроса, в первой части вопроса - на любом языке, лишь бы хорошая. Второй вопрос - существуют ли в принципе такие системы на Haskell.

А на каком языке написана исходная программа?

ни на каком - это LLVM Intermediate Representation

это не ограничение, это вторая часть вопроса, в первой части вопроса - на любом языке, лишь бы хорошая.

У меня небогатый опыт явного использования солверов (z3 и simplify), но, если что, ежегодно проводится измерение попугаев на известных бенчмарках — можно посмотреть их в таком порядке.

Один из участников активно продвигает Z3 от микрософта, но мне эта идея категорически не нравится (проект будет открыт)

ИМХО, есть смысл писать так, чтобы солвер менялся максимально безболезненно. Кто его знает, какой их них будет хорош в будущем (если вообще не будет заброшен)?