From: Tim King <taking@cs.nyu.edu>
Date: Mon, 11 Jun 2012 22:32:46 +0000 (+0000)
Subject: Fixing type comparision assertion in getEqualityStatus().
X-Git-Tag: cvc5-1.0.0~8080
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fbbd4e966395aa3c8094ef137aa17be5f372e2b0;p=cvc5.git

Fixing type comparision assertion in getEqualityStatus().
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7ea9e063e..a7c378152 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -997,7 +997,7 @@ void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) {
 }
 
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
-  Assert(a.getType() == b.getType());
+  Assert(a.getType().isComparableTo(b.getType()));
   if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) {
     if (d_sharedTerms.areEqual(a,b)) {
       return EQUALITY_TRUE_AND_PROPAGATED;