diff options
| author | Andres Nötzli <andres.noetzli@gmail.com> | 2017-06-30 11:39:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-06-30 11:39:17 -0700 |
| commit | ae4089fb6ff60fd5af5a212d68b91928f94bb5f2 (patch) | |
| tree | 7a68514dce79ca91f72f9245120517a391075d44 /NEWS | |
| parent | 303b91f3f5b8df1a884566a7d433ced17f0cd352 (diff) | |
Fix use-after-free with unsat cores/proofs (#174)
In TSatProof<Solver>::finalizeProof(), we got a clause from the clause
allocator, called resolveUnit() and then size() on the clause. The problem is
that resolveUnit() can reallocate memory (and there is even a comment warning
about that in finalizeProof()), which invalidates the clause. This commit gets
the clause again from the clause allocator before calling size().
Diffstat (limited to 'NEWS')
0 files changed, 0 insertions, 0 deletions