From ab98be633a17edcc6ebefa9667048c2e695ab5e1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Nov 2015 18:56:35 -0800
Subject: [PATCH] fix(library/blast/simplifier): warning when compiling using
 clang on OSX

---
 src/library/blast/simplifier.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index 7c5512c3d..a661d32bf 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -253,7 +253,8 @@ optional<result> simplifier::cache_lookup(expr const & e) {
     lean_assert(is_app(e_old));
     buffer<expr> new_args, old_args;
     expr const & f_new = get_app_args(e, new_args);
-    lean_verify(f_new == get_app_args(e_old, old_args));
+    DEBUG_CODE(expr const & f_old =) get_app_args(e_old, old_args);
+    lean_assert(f_new == f_old);
     auto congr_lemma = mk_congr_lemma(f_new, new_args.size());
     if (!congr_lemma) return optional<result>();
     expr proof = congr_lemma->get_proof();