Fix for iff terms over equalities between the same term and differing constants.

2 files changed, 9 insertions, 0 deletions

diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 8abaa5611..36f09f137 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -193,6 +193,10 @@ Cardinality::CardinalityComparison Cardinality::compare(const Cardinality& c) co
   Unreachable();
 }
 
+bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const throw() {
+  CardinalityComparison cmp = this->compare(c);
+  return cmp == LESS || cmp == EQUAL;
+}
 
 std::string Cardinality::toString() const throw() {
   std::stringstream ss;
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index c536ea065..c9d051c9e 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -245,6 +245,11 @@ public:
    */
   std::string toString() const throw();
 
+  /**
+   * Compare two cardinalities and if it is known that the current
+   * cardinality is smaller or equal to c, it returns true.
+   */
+  bool knownLessThanOrEqual(const Cardinality& c) const throw();
 };/* class Cardinality */