Re: [klee-dev] General question

[Cristian Cadar]

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,

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 
mailto:btssri...@gmail.com>> wrote:


Hello, I was wondering if there is way in which we can get
symbolic formula for a variable in a code in smt2 format unlike
kquery format which we get using klee_print_expr.
___
klee-dev mailing list
klee-dev@imperial.ac.uk 
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] General question

[Ferhat Erata]

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 which we can get
> symbolic formula for a variable in a code in smt2 format unlike
> kquery format which we get using klee_print_expr.
> ___
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] General question

[Teja Sai Srikar Bodavula]

Hello, I was wondering if there is way in which we can get symbolic formula
for a variable in a code in smt2 format unlike kquery format which we get
using klee_print_expr.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev