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 | |
| 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')
| -rw-r--r-- | src/smt/set_defaults.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 4ad198a82..79490045b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -963,6 +963,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { options::cegqiMidpoint.set(true); } + // must disable cegqi-bv since it may introduce witness terms, which + // cannot appear in synthesis solutions + if (!options::cegqiBv.wasSetByUser()) + { + options::cegqiBv.set(false); + } if (options::sygusRepairConst()) { if (!options::cegqi.wasSetByUser()) |