summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2012-06-11 22:32:46 +0000
committerTim King <taking@cs.nyu.edu>2012-06-11 22:32:46 +0000
commitfbbd4e966395aa3c8094ef137aa17be5f372e2b0 (patch)
treea0aa0bbc510cbbe2e6a4c25e57472a911e241782 /src/theory/theory_engine.cpp
parentdbe06dccdb08c816fd28266f44585e2d7f6a0a9f (diff)
Fixing type comparision assertion in getEqualityStatus().
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp2
1 files changed, 1 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback