From fdcdfbf385d37d000fec3b9a9f65cbf4ba9acdf3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 31 Dec 2015 14:25:38 -0800
Subject: [PATCH] feat(library/blast/simplifier/simplifier_actions): only add
 symplified hypothesis if it is not "true"

---
 src/library/blast/simplifier/simplifier_actions.cpp | 3 ++-
 src/library/util.cpp                                | 4 ++++
 src/library/util.h                                  | 1 +
 3 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/library/blast/simplifier/simplifier_actions.cpp b/src/library/blast/simplifier/simplifier_actions.cpp
index 8ff8d0819..0564d5dc1 100644
--- a/src/library/blast/simplifier/simplifier_actions.cpp
+++ b/src/library/blast/simplifier/simplifier_actions.cpp
@@ -118,7 +118,8 @@ action_result simplify_hypothesis_action(hypothesis_idx hidx) {
         // they are definitionally equal
         new_h_proof = h.get_self();
     }
-    s.mk_hypothesis(r.get_new(), new_h_proof);
+    if (!is_true(r.get_new()))
+        s.mk_hypothesis(r.get_new(), new_h_proof);
     s.del_hypothesis(hidx);
     return action_result::new_branch();
 }
diff --git a/src/library/util.cpp b/src/library/util.cpp
index ef463c726..82eecda78 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -418,6 +418,10 @@ expr mk_true() {
     return *g_true;
 }
 
+bool is_true(expr const & e) {
+    return e == *g_true;
+}
+
 expr mk_true_intro() {
     return *g_true_intro;
 }
diff --git a/src/library/util.h b/src/library/util.h
index c538308aa..2b6a1467e 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -110,6 +110,7 @@ level get_datatype_level(expr ind_type);
 expr instantiate_univ_param (expr const & e, name const & p, level const & l);
 
 expr mk_true();
+bool is_true(expr const & e);
 expr mk_true_intro();
 
 bool is_and(expr const & e, expr & arg1, expr & arg2);