From bcaebfa163bb27e1cf14c0f763afb47b185a5f99 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Mar 2020 16:19:31 -0500
Subject: [PATCH] Logic exception instead of assertion failure for instantiate
 (#4006)

Fixes #4003.

Protects against a (class of) nonsensical option combinations.
---
 src/theory/quantifiers/instantiate.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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
     {
-- 
2.30.2