Software Quality Assurance & Testing Stack Exchange is a question and answer site for software quality control experts, automation engineers, and software testers. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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!

share|improve this question
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
up vote 2 down vote accepted

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.

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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