diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-09 15:53:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-09 15:53:30 -0500 |
| commit | 6ed06a895c7e2c5b83c8fd470c1ee4cf42827a7f (patch) | |
| tree | b8f3866a1862f611246c06c43eb2cbfcdb6c667d /src/smt/smt_engine_scope.cpp | |
| parent | 9a939deab1a788b29b573ae7fb72a6088a1d7edf (diff) | |
(proof-new) Make proofs in term formula removal term context sensitive (#5008)
Previously term formula removal proofs didnt not take the term context into account. This updates it to make use of the term context sensitive support in TConvProofGenerator. More generally, it uses the term context computation as the standard way of caching the results of rewrites in this class (regardless of proofs).
Diffstat (limited to 'src/smt/smt_engine_scope.cpp')
0 files changed, 0 insertions, 0 deletions