[klee-dev] [KLEE-dev] printing queries in SMT2 format

sudiptac sudipta.chattopadhyay at liu.se
Tue Mar 31 14:57:04 BST 2015


Thanks a lot. We indeed figured out now that the ExprSMTLIBPrinter class 
is serving our
purpose.

Regards,
Sudipta

On 03/31/2015 03:22 PM, Dan Liew wrote:
> Hi,
>
> KLEE already has SMTLIBv2 printing support (I presume that's what you
> mean by SMT2). It is implemented in the ExprSMTLIBPrinter class [1].
>
> You can tell klee to log in this format using
> ``--use-query-log=all:smt2``. You can also convert .pc files to
> SMT-LIBv2 format using
> the ``kleaver`` tool using the the ``-print-smtlib`` command line option.
>
>
> Hope that helps.
>
> [1] https://github.com/klee/klee/blob/master/include/klee/util/ExprSMTLIBPrinter.h
>
> Thanks,
> Dan.




More information about the klee-dev mailing list