diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-11 12:39:38 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-11 12:39:38 -0600 |
| commit | 7d3198d18304eb6ea5f087a82defb4952fce31b9 (patch) | |
| tree | 8eb045184b7fcb1902c76c8cdb3fa75919872244 /examples/translator.cpp | |
| parent | 74aad1b10d0ed716624abfadf9cccc4ae7e4ba96 (diff) | |
Rewrite witness terms at prerewrite (#5419)
Ensures (witness ((x Int)) (= x (+ 1 a)) is rewritten to (+ 1 a), instead of e.g. (witness ((x Int)) (= a (- x 1)).
This is required for supporting purification skolems for arithmetic terms in the new proof architecture.
Diffstat (limited to 'examples/translator.cpp')
0 files changed, 0 insertions, 0 deletions