diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-27 13:40:18 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-27 18:40:18 +0000 |
| commit | 7461cd576c0ad4c19e996644157a63920c67649b (patch) | |
| tree | 55dcf2ce80bc8de77962fd7d9d8d1ad783715ca5 /src/theory/inference_id.h | |
| parent | 9c0ec4ead7a013c2da36c16d9d17471d921ca00e (diff) | |
Fix care graph computation for higher-order (#7474)
Since we apply a lazy schema for app completion, this may omit terms from the care graph that are relevant for theory combination. This corrects the care graph for UF when higher-order is enabled by considering the HO_APPLY version of all partially and fully applied prefixes of APPLY_UF terms during TheoryUF::computeCareGraph.
Fixes #5741. Fixes #5744. Fixes #5201. Fixes #5078. Fixes #4758.
Diffstat (limited to 'src/theory/inference_id.h')
0 files changed, 0 insertions, 0 deletions