diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-10 16:19:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-10 14:19:31 -0700 |
| commit | bcaebfa163bb27e1cf14c0f763afb47b185a5f99 (patch) | |
| tree | 062cd35bf77f36dbeff96725fedf08e0b0803aa4 | |
| parent | 03573865aaeaf434836d509724f5a8e8fc615fdd (diff) | |
Logic exception instead of assertion failure for instantiate (#4006)
Fixes #4003.
Protects against a (class of) nonsensical option combinations.
| -rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 2b56cff8f..9969de458 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -290,7 +290,10 @@ bool Instantiate::addInstantiation( { // virtual term substitution/instantiation level features are // incompatible - Assert(false); + std::stringstream ss; + ss << "Cannot combine instantiation strategies that require virtual term " + "substitution with those that restrict instantiation levels"; + throw LogicException(ss.str()); } else { |