From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 29 Jul 2019 16:57:09 +0000 (-0500)
Subject: Fix match trie for polymorphic operators (#3125)
X-Git-Tag: cvc5-1.0.0~4072
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3aba99657b39ccc0ab400c7ed9778673a3acddd7;p=cvc5.git

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 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);