Re: [klee-dev] Getting symbolic expressions from the symbolic store with `klee_print_expr`

2023-04-03 Thread Cristian Cadar
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

[klee-dev] Getting symbolic expressions from the symbolic store with `klee_print_expr`

2023-04-03 Thread Ferhat Erata
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