diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-16 12:04:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-16 17:04:39 +0000 |
| commit | 3d429c1187a2ac7d3270eddbbf5228002ad2740a (patch) | |
| tree | e91884b821d88cddb5b811c02d3a03fa35cb7315 /src/theory/theory_eq_notify.h | |
| parent | 6ed0dc4e833421e7da9345bda0196c598f852d29 (diff) | |
Do not exhaustive instantiation when FMF is disabled (#6899)
This makes FMF not handle quantified formulas when FMF options are disabled, apart from those marked internal.
This is required for combinations of sequences + quantified formulas.
Diffstat (limited to 'src/theory/theory_eq_notify.h')
0 files changed, 0 insertions, 0 deletions