Fix candidate rewrite utilities for non-first-class types (#2256)

diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index bf2248e259515a2f3e2de9f1abf5a5a638692db1..c49557fa9c5471a5dc4c3cf122ab98608d0b9583 100644 (file)
--- 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 d8c5ac7b5c135955031cb89810e9f5e0d8770c2f..f48f73aee15f621f01006a473a172d6ac26e0df2 100644 (file)
--- 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())