From faab1e449f167a194d0ef7df4e63f58ff554b5b1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jul 2015 17:01:19 -0700
Subject: [PATCH] fix(tests/lean/rw_set3): update test to reflect changes in
 the standard library

---
 tests/lean/rw_set3.lean.expected.out | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/tests/lean/rw_set3.lean.expected.out b/tests/lean/rw_set3.lean.expected.out
index df6fc53e3..f9e6ae968 100644
--- a/tests/lean/rw_set3.lean.expected.out
+++ b/tests/lean/rw_set3.lean.expected.out
@@ -1,18 +1,29 @@
 simplification rules for iff
+#1, ?M_1 ↔ false ↦ ¬?M_1
+#1, ?M_1 ↔ true ↦ ?M_1
+#0, false ↔ true ↦ false
+#0, true ↔ false ↦ false
+#1, ?M_1 ↔ ¬?M_1 ↦ false
 #1, ?M_1 ↔ ?M_1 ↦ true
 #1, false ↔ ?M_1 ↦ ¬?M_1
-#1, ?M_1 ↔ false ↦ ¬?M_1
 #1, true ↔ ?M_1 ↦ ?M_1
-#1, ?M_1 ↔ true ↦ ?M_1
+#3 perm, ?M_1 ∧ ?M_2 ∧ ?M_3 ↦ ?M_2 ∧ ?M_1 ∧ ?M_3
 #1, ?M_1 ∧ ?M_1 ↦ ?M_1
 #1, false ∧ ?M_1 ↦ false
 #1, ?M_1 ∧ false ↦ false
 #1, true ∧ ?M_1 ↦ ?M_1
 #1, ?M_1 ∧ true ↦ ?M_1
+#3, (?M_1 ∧ ?M_2) ∧ ?M_3 ↦ ?M_1 ∧ ?M_2 ∧ ?M_3
+#2 perm, ?M_1 ∧ ?M_2 ↦ ?M_2 ∧ ?M_1
+#2, ?M_2 == ?M_2 ↦ true
+#3 perm, ?M_1 ∨ ?M_2 ∨ ?M_3 ↦ ?M_2 ∨ ?M_1 ∨ ?M_3
 #1, false ∨ ?M_1 ↦ ?M_1
 #1, ?M_1 ∨ false ↦ ?M_1
 #1, true ∨ ?M_1 ↦ true
 #1, ?M_1 ∨ true ↦ true
+#3, (?M_1 ∨ ?M_2) ∨ ?M_3 ↦ ?M_1 ∨ ?M_2 ∨ ?M_3
+#2 perm, ?M_1 ∨ ?M_2 ↦ ?M_2 ∨ ?M_1
+#2, ?M_2 = ?M_2 ↦ true
 #0, ¬false ↦ true
 #0, ¬true ↦ false
 simplification rules for eq