search

tracer-x / TracerX

TracerX Symbolic Virtual Machine
https://tracer-x.github.io/
Other
31 stars 11 forks source link

Over-marking of path condition #293

Closed domainexpert closed 7 years ago

domainexpert commented 7 years ago

Regarding the over-marking in overmark.c of tracer-x/klee-examples#136. This is caused by marking in a common parent of a constraint in the path condition, which is not used in one of the children, causing unnecessarily strong stored interpolant.

Credits to @rasoolmaghareh for discovering this issue, and to Joxan Jaffar for discussions.

Note this issue was resolved in TRACER by having separate markings for the children in a branch of the execution tree.

domainexpert commented 7 years ago

@rasoolmaghareh I say it again: You're the man!

Resolved via #294.