diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-22 09:23:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-22 09:23:57 -0500 |
| commit | c98ba7775ecb8a192e2a93735885163234546be3 (patch) | |
| tree | fbfef218b03aeb1aa762da05785fe1d59ef43625 /src/theory/strings/inference_manager.cpp | |
| parent | 37107284adaad3d24da0ad15cac8c88af444aeef (diff) | |
Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)
Fixes #4092 and fixes #4134.
Typically, APPLY_UF has special treatment in sort inference. It is significantly more complicated when higher-order logic is enabled. This disables special handling when ufHo() is enabled.
Diffstat (limited to 'src/theory/strings/inference_manager.cpp')
0 files changed, 0 insertions, 0 deletions