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

Dan Liew dan at su-root.co.uk
Tue Mar 31 14:22:21 BST 2015


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