Fix match trie for polymorphic operators (#3125)

diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index 53c40464fc0e5570b6740eed89f44bedff5e25a7..c07cae51d133dd79b94c5e3eb745624a1dfdbb90 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -135,6 +135,10 @@ bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
               recurse = false;
             }
           }
+          else if (!var.getType().isSubtypeOf(cn.getType()))
+          {
+            recurse = false;
+          }
           else
           {
             vars.push_back(var);