fix(library/simplifier/simplifier): bug in cache_lookup

This commit is contained in:
Leonardo de Moura 2016-01-06 17:30:01 -08:00
parent 14d4ae7e97
commit e7bcb89314

View file

@ -257,6 +257,8 @@ public:
/* Cache */
optional<result> simplifier::cache_lookup(expr const & e) {
/* cache_lookup is based on congr_lemma, and assumes \c e is an application */
if (!is_app(e)) return optional<result>();
auto it = m_cache.find(key(m_rel, e));
if (it == m_cache.end()) return optional<result>();
/* The cache ignores subsingletons, so we may need to