diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-08 15:55:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-08 15:55:32 -0600 |
| commit | ca9705cf0785e3a81fc25995df0bc3dc76e3bd9f (patch) | |
| tree | 89359d3de3099cae4557aabc2a23f342098b09c6 /src/theory/quantifiers/instantiate.h | |
| parent | 2ba8c852864ecb2eea3be2253fb80af1328de158 (diff) | |
Fix disequality between seq.unit terms (#5880)
This adds a missing inference for disequality between seq.unit terms, which was not handled previously.
Fixes #5666.
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
0 files changed, 0 insertions, 0 deletions