diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-11 15:04:35 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-11 15:04:35 -0600 |
| commit | 49215e6948aba1d6b762e28a7293581e25c2df8c (patch) | |
| tree | c769369b913bb383c714ae68c575add32e3d06e1 /src/prop/theory_proxy.cpp | |
| parent | e4fd524b02054a3ac9724f184e55a983cb6cb6b9 (diff) | |
Fix length assumption for deq norm emp rule (#5623)
There is an assumption that is not guaranteed to hold in this rule, thus we should not try to explain in the equality engine.
Fixes #5611.
Note this inference was not previously covered in our coverage build.
Diffstat (limited to 'src/prop/theory_proxy.cpp')
0 files changed, 0 insertions, 0 deletions