From 1e436b8b3e299ff0711063eeff1e5039fec83479 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Nov 2015 16:28:09 -0800 Subject: [PATCH] fix(library/blast/state): incorrect assertions --- src/library/blast/state.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 5e62d13018..232a317b37 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -298,7 +298,6 @@ public: } level const * get_uref_assignment(level const & l) const { - lean_assert(is_uref_assigned(l)); return m_uassignment.find(uref_index(l)); } @@ -316,7 +315,6 @@ public: bool has_assigned_uref(levels const & ls) const; expr const * get_mref_assignment(expr const & e) const { - lean_assert(is_mref(e)); return m_eassignment.find(mref_index(e)); }