From 3aba99657b39ccc0ab400c7ed9778673a3acddd7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 29 Jul 2019 11:57:09 -0500 Subject: [PATCH] Fix match trie for polymorphic operators (#3125) --- src/theory/quantifiers/candidate_rewrite_filter.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index 53c40464f..c07cae51d 100644 --- 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); -- 2.30.2