diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-23 14:56:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-23 14:56:52 -0500 |
| commit | aacc90c1234c488f49814fae6dbf0e720e2dfa88 (patch) | |
| tree | 4d147316d0d8e8d570f96c43d4f03bba9d0db06a /src/theory/inference_manager_buffered.h | |
| parent | 770d9ae622ec04bc2fbea8356ce11329ed06fa5b (diff) | |
Disable cegqi-bv when using sygus (#5124)
This disables the CAV 2018 techniques for BV quantifier instantiation when solving sygus since they may generate terms with witness in them. This adds a regression where this occurs.
I've opened an cvc4 projects issue to revisit this (CVC4/cvc4-projects#227).
Diffstat (limited to 'src/theory/inference_manager_buffered.h')
0 files changed, 0 insertions, 0 deletions