From 94f8bafb38ccf380ace36259026a3b0959d13636 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Apr 2020 03:02:50 -0500
Subject: [PATCH] Fix assertion in enumerative instantiation (#4313)

Fixes regress1.
---
 src/theory/quantifiers/inst_strategy_enumerative.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 81ade68fc..6c17746ef 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -313,7 +313,8 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
                   << "  " << term_db_list[ftypes[i]][childIndex[i]]
                   << std::endl;
             }
-            Assert(terms[i].getType().isComparableTo(ftypes[i]));
+            Assert(terms[i].isNull()
+                   || terms[i].getType().isComparableTo(ftypes[i]));
           }
           if (ie->addInstantiation(f, terms))
           {
-- 
2.30.2