From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 20 Mar 2020 20:36:35 +0000 (-0500)
Subject: Fix sort comparison within assertion in cegis (#4113)
X-Git-Tag: cvc5-1.0.0~3463
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=537bb89c664375aa0fe0143e65d255de34bd611c;p=cvc5.git

Fix sort comparison within assertion in cegis (#4113)
---

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 57fe40517..dfef0bad4 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -599,7 +599,7 @@ bool Cegis::checkRefinementEvalLemmas(const std::vector<Node>& vs,
       for (unsigned j = 0, psize = vsProc.size(); j < psize; j++)
       {
         evalVisited[vsProc[j]] = msProc[j];
-        Assert(vsProc[j].getType() == msProc[j].getType());
+        Assert(vsProc[j].getType().isComparableTo(msProc[j].getType()));
       }
     }
   }