From 96f6bf70284156529d258c679fe361aeb16900af Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Mon, 15 Feb 2016 12:06:20 +0000
Subject: [PATCH] ctx_simplify: simplify ite if then/else values become equal

---
 src/tactic/core/ctx_simplify_tactic.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index c61f2d3af..c0453cf0e 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -430,7 +430,10 @@ struct ctx_simplify_tactic::imp {
             simplify(e, new_e);
             pop(scope_level() - old_lvl);
             if (c == new_c && t == new_t && e == new_e) {
-                r     = ite;
+                r = ite;
+            }
+            else if (new_t == new_e) {
+                r = new_t;
             }
             else {
                 expr * args[3] = { new_c.get(), new_t.get(), new_e.get() };