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 /configure.sh | |
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 'configure.sh')
0 files changed, 0 insertions, 0 deletions