projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 306ca2f) | patch
Fix proofs for datatype purify (#7841)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 4 Jan 2022 21:50:17 +0000 (15:50 -0600)
committerGitHub <noreply@github.com>
Tue, 4 Jan 2022 21:50:17 +0000 (21:50 +0000)
commitbc61a1d1b0fa893ecfb4f62557916357773b5987
treea67831fe1a9399cbafe1c6d300713cb7e6c46e67tree
parent306ca2f784980ace13aa5c9149bf067b0a1c54fecommit | diff
Fix proofs for datatype purify (#7841)

Previously we were failing to produce proofs for purification lemmas (= t witness_form(t)) from datatypes.
src/theory/datatypes/infer_proof_cons.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history