KLEE function: markBranchVisited

[Super Zhang]

Hi all,

In KLEE, markBranchVisited is called whenever a branch
is visited through fork/branch. My question is that can we say this branch
is definitely reachable if it ever has been marked as visited?

Thanks,
Chaoqiang

[Super Zhang]

To be specific, after seeding stage of KLEE, the constraints in the
remaining states(to be explored further) are definitely will be true or
just possibly be true?

Thanks,
Chaoqiang

Post by Super Zhang
Hi all,
In KLEE, markBranchVisited is called whenever a branch
is visited through fork/branch. My question is that can we say this branch
is definitely reachable if it ever has been marked as visited?
Thanks,
Chaoqiang