diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2017-05-24 13:28:58 -0700 |
---|---|---|
committer | Andres Nötzli <andres.noetzli@gmail.com> | 2017-05-26 01:47:00 -0700 |
commit | 0a425613d5108efa5f623d075135f2e08d3dfde2 (patch) | |
tree | 041568ac9d317a6672c81f730d6d7f512248cc83 /src/theory | |
parent | 97443967555b0e7fe6be4e6ab03b81383bc90430 (diff) |
Fix use-after-free with ResChains
This commit fixes an issue where the ResChain in `d_resolutionChains` gets
deleted here:
https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L729
The condition immediately after is false because the condition on line 727 is
true. Thus, `d_resolutionChains` now has a deleted entry for `id`.
When CVC4 afterwards gets the ResChain associated with `id` in
`checkResolution()`, it accesses the deleted entry:
https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L303
Diffstat (limited to 'src/theory')
0 files changed, 0 insertions, 0 deletions