Option to dump formulas passed to the SMT solver
35 views
Skip to first unread message
Marcelo Sousa
May 16, 2012, 8:52:10 AM5/16/12
to LLBMC
Hello,
I'm interested on analyzing the formula passed to the SMT solver. As
far as I can see from the help of llbmc there is no flag to dump that
information.
Is it possible to add that functionality to the tool or give some
insight on how to get it?
Kind regards,
Marcelo Sousa
I'm interested on analyzing the formula passed to the SMT solver. As
far as I can see from the help of llbmc there is no flag to dump that
information.
Is it possible to add that functionality to the tool or give some
insight on how to get it?
Kind regards,
Marcelo Sousa
Florian Merz
May 16, 2012, 10:36:43 AM5/16/12
to LLBMC
Hi Marcelo,
as far as I remember, this is not possible in the released version of
LLBMC. The reason for this is that we use the SMT solvers' C APIs
directly.
In our current development version we added support for dumping to
SMTLIB and SMTLIB2 format. We hope to provide a new release of LLBMC
soon which will include this feature.
Bes regards,
Florian Merz
as far as I remember, this is not possible in the released version of
LLBMC. The reason for this is that we use the SMT solvers' C APIs
directly.
In our current development version we added support for dumping to
SMTLIB and SMTLIB2 format. We hope to provide a new release of LLBMC
soon which will include this feature.
Bes regards,
Florian Merz
Reply all
Reply to author
Forward
0 new messages