[klee-dev] Experssion Rewriter

[Zhiyi Zhang]

Hi, Rizzi

Thank you for your reply.

I have read the file in
https://github.com/klee/klee/commit/f0de5e4ea4f1bed2e698ae99a19f1f0b96770f9c,
but I am confused that this file seems also to be used for constraint set
simplification optimization. Does expression rewrite optimization and
constraint
set simplification optimization have combined in the new version? And the
option is --rewrite-equalities and --equality-substitution?

Best wishes.
Zhiyi Zhang

On Mon, May 11, 2015 at 7:54 PM, Eric Rizzi <eric.rizzi at gmail.com> wrote:

> There should be a --rewrite-equalities option per the following commit
>
>
> https://github.com/klee/klee/commit/f0de5e4ea4f1bed2e698ae99a19f1f0b96770f9c
>
> The default behavior is on anyways, though.
>
> On Mon, May 11, 2015 at 3:02 AM, Zhiyi Zhang <xianlingzibiying at gmail.com>
> wrote:
>
>> Hi all,
>>
>> When I used klee with llvm3.4, I found that there is no "--rewrite"
>> option in klee orders. So how could I use expression  rewrite optimization
>>  when I use klee running a program?
>>
>> Thank you.
>> Zhiyi Zhang
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
>
-------------- next part --------------
HTML attachment scrubbed and removed