diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-12 10:00:36 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-12 10:00:36 -0600 |
| commit | b9eee8d69e9de4641514c35d49c495bd5adead5f (patch) | |
| tree | 493aff91499c84e1b3543f34c679b2c6f1aa2d17 /cmake/FindGLPK.cmake | |
| parent | 2de877854e590e8edf89ffb1d940cd4c9717f195 (diff) | |
(proof-new) Fix true explanations of propagations in pf equality engine (#5338)
This ensures we construct proper proofs for propagations whose conclusions are of the form (=> true lit). Literals may be propagated with "true" as an explanation in datatypes, e.g. discriminators for datatypes with 1 constructor.
Diffstat (limited to 'cmake/FindGLPK.cmake')
0 files changed, 0 insertions, 0 deletions