search

tracer-x / TracerX

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

Remove quantification in case the body of a quantified query expression has no constraint with both bound and non-bound variables #292

Closed domainexpert closed 7 years ago

domainexpert commented 7 years ago

In SubsumptionTableEntry::subsumed() remove quantification in case the body of a quantified query expression has no constraint with both bound and non-bound variables.

This resolves #288. For basic/arraysimple5.c for fp-examples, there is a reduction in subsumption count from 17 with tracer-x/klee@bf6461a3edc074016f4173d72a3cea699352c841 to 14 with this PR, but the space traversed decreased from 307 instructions to only 195 instructions. There are increases in subsumption counts for basic/regexp_iterative.c and basic/sp.c.

make check succeeds.