diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-15 23:51:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-15 21:51:51 -0700 |
| commit | 227cd8c26c508b7b444fbed6f2868f90c8281eed (patch) | |
| tree | f48f18c8bda3c4ad448c711a7316f813c3819cb4 /src/theory/uf/equality_engine.cpp | |
| parent | 442ab0cdd8578631974318c17dd8ace59d145839 (diff) | |
Handle cases in --sygus-rr where evaluation is not constant (#4100)
Throws warning instead of error if two terms with the same rewritten form evaluate differently, but the evaluation is non-constant.
Fixes #4096 and fixes #4089.
Diffstat (limited to 'src/theory/uf/equality_engine.cpp')
0 files changed, 0 insertions, 0 deletions