GaloisInc / pate

Patches Assured up to Trace Equivalence
Other
14 stars 3 forks source link

actively prune redundant path conditions #251

Closed danmatichuk closed 2 years ago

danmatichuk commented 2 years ago
* use the solver during path condition generation to
  avoid adding path conditions that are implied by
  the current assumption state

* uses some of the structured equivalence changes to simplify
  register traversal

depends on #249 addresses missing path condition for #206