diff options
| -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 { |