From 768a45b7f906572b427bf6df7c62cf2fbd377aa9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Sep 2018 16:21:37 -0700 Subject: [PATCH] feat(library/compiler/csimp): avoid unnecessary let-decls --- src/library/compiler/csimp.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index 0fb6232c30..3ba564e5b8 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -60,10 +60,14 @@ class csimp_fn { } expr mk_let_decl(expr const & e) { - expr type = infer_type(e); - expr fvar = m_lctx.mk_local_decl(ngen(), next_name(), type, e); - m_fvars.push_back(fvar); - return fvar; + if (is_atom(e)) { + return e; + } else { + expr type = infer_type(e); + expr fvar = m_lctx.mk_local_decl(ngen(), next_name(), type, e); + m_fvars.push_back(fvar); + return fvar; + } } expr visit_let(expr e) {