I am reading the slides of a famous random test+symbolic execution software test tool cute's slides.

In one slide, I see this claim on classic symbolic execution:

enter image description here

So my question is :

Why author claims that "Symbolic execution will say both branches are reachable"?

From my understanding, symbolic execution needs to solve the constrains of branch conditions, and basically


else statement's constrain can not be solved, am I right?

Could anyone give me some help?

Thank you!

  • The author claimed that Existing Approach II waa\s not capable of that kind of reasoning. It might help for you to determine what the author meant by "Existing Approach II". Perhaps the state of the art in symbolic execution has changed in the last ten years.
    – user246
    Feb 28 '14 at 17:16

The symbolic solver in the slide cannot deduce that an integer multiplied by 4 cannot be 17. This is a statement about that particular solver at that point in time, not about solvers in general.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.