Hi Ferhat,
Essentially, you want something like this:
printer.printExpression(arguments[1], ExprSMTLIBPrinter::SORT_BITVECTOR);
To do this right requires a bit more work, but as a quick proof of
concept, just change the visibility of this method.
Best,
Cristian
On 03/04/2023 01:39, Ferhat
Hi both,
Let me answer this as part of the more detailed email Ferhat sent today.
But more generally, you can use Kleaver to load queries in KQuery format
and print them to SMT-LIB2 format:
kleaver --print-smtlib file.kquery
Best,
Cristian
On 30/03/2023 21:57, Ferhat Erata wrote:
Hi Teja,
Hi Teja,
I was also looking for this feature. Have you come up with a workaround?
Do you know if there is a way to transform expressions in kquery format to
smt2 format?
Best,
~ Ferhat
On Mon, Jan 9, 2023 at 7:21 AM Teja Sai Srikar Bodavula
wrote:
> Hello, I was wondering if there is way in
Hi,
I wanted to ask about converting symbolic expressions in KQuery format
to SMTLIB format.
Currently, I am able to obtain the symbolic expressions using
`klee_print_expr` in KQuery format, but I need to manipulate them in
bit-vector logic, which requires converting them to SMTLIB format to
