From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Mar 2020 21:19:31 +0000 (-0500)
Subject: Logic exception instead of assertion failure for instantiate (#4006)
X-Git-Tag: cvc5-1.0.0~3524
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bcaebfa163bb27e1cf14c0f763afb47b185a5f99;p=cvc5.git

Logic exception instead of assertion failure for instantiate (#4006)

Fixes #4003.

Protects against a (class of) nonsensical option combinations.
---

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
     {