From c03a972a85d565f10953ee58ec809f1751063f8e Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 13 Mar 2013 20:37:57 -0400
Subject: [PATCH] Added a rewrite for iff: x = c iff x = d ---> false This
 fixes Andy's problem if unconstrained simplification is turned on.

---
 src/theory/booleans/theory_bool_rewriter.cpp | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 567a8dd70..2fa2e095a 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -118,6 +118,24 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
       // IFF x (NOT x)
       return RewriteResponse(REWRITE_DONE, ff);
+    } else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) {
+      TNode t,c;
+      if (n[0][0].isConst()) {
+        c = n[0][0];
+        t = n[0][1];
+      }
+      else if (n[0][1].isConst()) {
+        c = n[0][1];
+        t = n[0][0];
+      }
+      if (!c.isNull()) {
+        if (n[1][0] == t && n[1][1].isConst()) {
+          return RewriteResponse(REWRITE_DONE, n[1][1] == c ? tt : ff);
+        }
+        else if (n[1][1] == t && n[1][0].isConst()) {
+          return RewriteResponse(REWRITE_DONE, n[1][0] == c ? tt : ff);
+        }
+      }
     }
     break;
   }
-- 
2.30.2