From 493bf7a8619e5779604fb73aa6a0b7000a529d6a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 2 Aug 2018 14:54:37 -0500
Subject: [PATCH] Fix candidate rewrite utilities for non-first-class types
 (#2256)

---
 .../quantifiers/candidate_rewrite_filter.cpp  | 21 +++++++++++++------
 src/theory/quantifiers/dynamic_rewrite.cpp    |  4 ++++
 2 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index bf2248e25..c49557fa9 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -161,6 +161,7 @@ bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
 
 void MatchTrie::addTerm(Node n)
 {
+  Assert(!n.isNull());
   std::vector<Node> visit;
   visit.push_back(n);
   MatchTrie* curr = this;
@@ -301,13 +302,18 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
     Trace("crf-match") << "CRF check matches : " << bn << " [rhs = " << beq_n
                        << "]..." << std::endl;
     Node bni = d_drewrite->toInternal(bn);
-    if (!d_match_trie.getMatches(bni, &d_ssenm))
+    if (!bni.isNull())
     {
-      keep = false;
-      Trace("cr-filter") << "...redundant (matchable)" << std::endl;
-      // regardless, would help to remember it
-      registerRelevantPair(n, eq_n);
+      if (!d_match_trie.getMatches(bni, &d_ssenm))
+      {
+        keep = false;
+        Trace("cr-filter") << "...redundant (matchable)" << std::endl;
+        // regardless, would help to remember it
+        registerRelevantPair(n, eq_n);
+      }
     }
+    // if bni is null, it may involve non-first-class types that we cannot
+    // reason about
   }
 
   if (keep)
@@ -356,7 +362,10 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n)
       {
         Trace("crf-match") << "CRF add term : " << t << std::endl;
         Node ti = d_drewrite->toInternal(t);
-        d_match_trie.addTerm(ti);
+        if (!ti.isNull())
+        {
+          d_match_trie.addTerm(ti);
+        }
       }
       d_pairs[t].insert(to);
     }
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index d8c5ac7b5..f48f73aee 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -109,6 +109,10 @@ Node DynamicRewriter::toInternal(Node a)
     for (const Node& ca : a)
     {
       Node cai = toInternal(ca);
+      if (cai.isNull())
+      {
+        return Node::null();
+      }
       children.push_back(cai);
     }
     if (!children.empty())
-- 
2.30.2