From 9a8d0af063302752905bda7f2043a9695c3126d3 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Wed, 28 Mar 2012 15:28:38 +0000
Subject: [PATCH] getting rid of a rewrite in uf sharing, speeds things up a
 bit

---
 src/theory/uf/theory_uf.cpp | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index a3e347b90..4ac81bc74 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -397,22 +397,18 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 
 EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
 
-  Node equality = a.eqNode(b);
-  Node rewrittenEquality = Rewriter::rewrite(equality);
-  if (rewrittenEquality.isConst()) {
-    if (!rewrittenEquality.getConst<bool>()) {
-      return EQUALITY_FALSE;
-    }
-  }
-
+  // Check for equality (simplest)
   if (d_equalityEngine.areEqual(a, b)) {
     // The terms are implied to be equal
     return EQUALITY_TRUE;
   }
+
+  // Check for disequality
   if (d_equalityEngine.areDisequal(a, b)) {
     // The terms are implied to be dis-equal
     return EQUALITY_FALSE;
   }
+
   // All other terms we interpret as dis-equal in the model
   return EQUALITY_FALSE_IN_MODEL;
 }
-- 
2.30.2