From 18f224c4204d3500fae1943f43417a492ab087ae Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Mon, 7 Dec 2015 11:44:10 -0800
Subject: [PATCH] fix(library/blast/actions/simple_actions): fix assert

---
 src/library/blast/actions/simple_actions.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/blast/actions/simple_actions.cpp b/src/library/blast/actions/simple_actions.cpp
index 446ec831a..943ec4acc 100644
--- a/src/library/blast/actions/simple_actions.cpp
+++ b/src/library/blast/actions/simple_actions.cpp
@@ -90,7 +90,7 @@ action_result assumption_contradiction_actions(hypothesis_idx hidx) {
                 if (num_not1 > num_not2) {
                     return action_result(b.mk_app(get_absurd_name(), {s.get_target(), pr2, pr1}));
                 } else {
-                    lean_assert(is_neg2);
+                    lean_assert(num_not1 < num_not2);
                     return action_result(b.mk_app(get_absurd_name(), {s.get_target(), pr1, pr2}));
                 }
             }