Re: [klee-dev] Why is ConstraintSet not a set?

2023-07-14 Thread Nguyễn Gia Phong
On 2023-07-12 at 22:03+01:00, Cristian Cadar wrote:
> On 07/07/2023 06:57, Nguyễn Gia Phong wrote:
> > I notice that ConstraintSet is implemented via std::vector.
> > This make me wonder about the likelihood of duplucated constraints
> > during executions.
>
> KLEE does not add duplicate constraints, in fact it does not add a 
> constraint if it is implied by the current PC.

Thanks, I see the check now.

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


Re: [klee-dev] Why is ConstraintSet not a set?

2023-07-12 Thread Cristian Cadar

Hi,

KLEE does not add duplicate constraints, in fact it does not add a 
constraint if it is implied by the current PC.


Best,
Cristian

On 07/07/2023 06:57, Nguyễn Gia Phong wrote:

Hi,

I notice that ConstraintSet is implemented via std::vector.
This make me wonder about the likelihood of duplucated constraints
during executions.

Does anyone have any emprical data or experience regarding this aspect?

Regards,
McSinyx

___
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] Why is ConstraintSet not a set?

2023-07-07 Thread Nguyễn Gia Phong
Hi,

I notice that ConstraintSet is implemented via std::vector.
This make me wonder about the likelihood of duplucated constraints
during executions.

Does anyone have any emprical data or experience regarding this aspect?

Regards,
McSinyx

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