Fix for bug 447.

1 files changed, 14 insertions, 0 deletions

diff --git a/src/util/result.cpp b/src/util/result.cpp
index f51bacee7..6a32747cb 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -92,6 +92,20 @@ bool Result::operator==(const Result& r) const throw() {
   return false;
 }
 
+bool operator==(enum Result::Sat sr, const Result& r) throw() {
+  return r == sr;
+}
+
+bool operator==(enum Result::Validity vr, const Result& r) throw() {
+  return r == vr;
+}
+bool operator!=(enum Result::Sat s, const Result& r) throw(){
+  return !(s == r);
+}
+bool operator!=(enum Result::Validity v, const Result& r) throw(){
+  return !(v == r);
+}
+
 Result Result::asSatisfiabilityResult() const throw() {
   if(d_which == TYPE_SAT) {
     return *this;