diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-17 21:06:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-17 21:06:44 -0500 |
| commit | cb438c1aca9e205359313f2e661fef910e1132b6 (patch) | |
| tree | c13f405d9065846619fcc8e1008bfa3433542a13 /src/smt/proof_post_processor.cpp | |
| parent | 6341581d4b6797e8a9169a2ad88638987da255a4 (diff) | |
(proof-new) Rewrites involving operators in term conversion proof generator (#5072)
In some cases, e.g. witness form conversion, we require traversing to operators in term conversion proofs. This updates the term conversion generator to support (term-context-sensitive) rewrites involving operators using HO_CONG. This requires updating the term context utilities with support for operators.
Diffstat (limited to 'src/smt/proof_post_processor.cpp')
0 files changed, 0 insertions, 0 deletions