From 2e970d67ba916fd1fd724b076d9d6fcf79a98de3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 May 2016 17:17:45 -0700 Subject: [PATCH] fix(compiler/preprocess_rec): add extra comp_irrelevant step --- src/compiler/preprocess_rec.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/compiler/preprocess_rec.cpp b/src/compiler/preprocess_rec.cpp index 2184f3715f..a41a6db59a 100644 --- a/src/compiler/preprocess_rec.cpp +++ b/src/compiler/preprocess_rec.cpp @@ -113,6 +113,7 @@ public: v = eta_expand(m_env, v); v = simp_pr1_rec(m_env, v); v = inline_simple_definitions(m_env, v); + v = mark_comp_irrelevant_subterms(m_env, v); v = lambda_lifting(m_env, v, m_aux_decls, d.is_trusted()); display(v); // TODO(Leo)