From f9624b4c49ad3a84010cd92bd438b1a32396bb3a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 May 2016 17:52:42 -0700 Subject: [PATCH] fix(library/compiler/vm_compiler): ignore applications of the form (neutral ...) during code generation --- src/library/compiler/vm_compiler.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index d4c2329566..e59ebebe9f 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -189,7 +189,9 @@ class vm_compiler_fn { emit_apply_instr(args.size()); return; } else if (is_constant(fn)) { - if (optional decl = get_vm_decl(m_env, const_name(fn))) { + if (is_neutral_expr(fn)) { + emit(mk_sconstructor_instr(0)); + } else if (optional decl = get_vm_decl(m_env, const_name(fn))) { compile_global(*decl, args.size(), args.data(), bpz, m); } else { throw_unknown_constant(const_name(fn));