From bf7f728381bb27163f3e056d698ba4da6316b9c8 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Mon, 1 Apr 2013 15:23:46 -0400
Subject: [PATCH] fixed TheoryBool rewriter bug

---
 src/theory/booleans/theory_bool_rewriter.cpp | 40 +++++++-------
 test/regress/regress0/incorrect1.smt         | 57 ++++++++++++++++++++
 2 files changed, 79 insertions(+), 18 deletions(-)
 create mode 100644 test/regress/regress0/incorrect1.smt

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 2fa2e095a..967126da1 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -118,25 +118,29 @@ 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);
-        }
-      }
     }
+    // This is wrong: it would rewrite c1 == x <=> c2 == x to false
+    // when this is sat for x = c3 where c3 is different from c1, and c2
+    
+    // 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;
   }
   case kind::XOR: {
diff --git a/test/regress/regress0/incorrect1.smt b/test/regress/regress0/incorrect1.smt
new file mode 100644
index 000000000..f1352334c
--- /dev/null
+++ b/test/regress/regress0/incorrect1.smt
@@ -0,0 +1,57 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:status unknown
+:extrafuns ((v0 BitVec[10]))
+:formula
+(let (?e1 bv30369[16])
+(let (?e2 bv3[2])
+(let (?e3 (ite (bvule ?e1 ?e1) bv1[1] bv0[1]))
+(let (?e4 (bvcomp (zero_extend[1] ?e3) ?e2))
+(let (?e5 (ite (bvsgt (sign_extend[15] ?e4) ?e1) bv1[1] bv0[1]))
+(let (?e6 (bvsmod ?e1 ?e1))
+(let (?e7 (bvsdiv v0 v0))
+(flet ($e8 (bvult ?e2 ?e2))
+(flet ($e9 (bvsge ?e7 (zero_extend[9] ?e3)))
+(flet ($e10 (bvugt (sign_extend[15] ?e4) ?e6))
+(flet ($e11 (bvsgt (sign_extend[15] ?e3) ?e6))
+(flet ($e12 (bvsgt v0 (sign_extend[9] ?e3)))
+(flet ($e13 (bvsgt ?e4 ?e4))
+(flet ($e14 (bvsle ?e1 (zero_extend[14] ?e2)))
+(flet ($e15 (bvslt (sign_extend[14] ?e2) ?e6))
+(flet ($e16 (bvslt (zero_extend[9] ?e3) ?e7))
+(flet ($e17 (= ?e6 (sign_extend[15] ?e3)))
+(flet ($e18 (= (zero_extend[8] ?e2) v0))
+(flet ($e19 (bvsgt ?e2 (sign_extend[1] ?e3)))
+(flet ($e20 (bvslt ?e3 ?e4))
+(flet ($e21 (bvslt ?e6 (zero_extend[15] ?e4)))
+(flet ($e22 (distinct (zero_extend[9] ?e4) v0))
+(flet ($e23 (bvuge ?e1 (sign_extend[15] ?e5)))
+(flet ($e24 (or $e12 $e19))
+(flet ($e25 (implies $e16 $e8))
+(flet ($e26 (and $e14 $e20))
+(flet ($e27 (not $e13))
+(flet ($e28 (not $e22))
+(flet ($e29 (xor $e11 $e23))
+(flet ($e30 (or $e29 $e15))
+(flet ($e31 (not $e26))
+(flet ($e32 (iff $e31 $e18))
+(flet ($e33 (and $e27 $e17))
+(flet ($e34 (xor $e21 $e10))
+(flet ($e35 (xor $e32 $e33))
+(flet ($e36 (and $e30 $e30))
+(flet ($e37 (xor $e9 $e9))
+(flet ($e38 (xor $e36 $e34))
+(flet ($e39 (or $e24 $e25))
+(flet ($e40 (iff $e38 $e28))
+(flet ($e41 (iff $e40 $e35))
+(flet ($e42 (not $e37))
+(flet ($e43 (and $e42 $e42))
+(flet ($e44 (iff $e43 $e41))
+(flet ($e45 (iff $e39 $e44))
+(flet ($e46 (and $e45 (not (= v0 bv0[10]))))
+(flet ($e47 (and $e46 (not (= v0 (bvnot bv0[10])))))
+(flet ($e48 (and $e47 (not (= ?e1 bv0[16]))))
+(flet ($e49 (and $e48 (not (= ?e1 (bvnot bv0[16])))))
+$e49
+))))))))))))))))))))))))))))))))))))))))))))))))))
+
-- 
2.30.2