From 8a0b2534bb9d54c1201ba6f18a643ae9a1bc0618 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 May 2016 19:35:28 -0700
Subject: [PATCH] fix(library/vm/vm): builtin function invocation

---
 src/frontends/lean/builtin_cmds.cpp | 1 +
 src/library/vm/vm.cpp               | 9 +++++++--
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 2f11768a2d..b8d1e685d9 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -669,6 +669,7 @@ static environment vm_eval_cmd(parser & p) {
     s.invoke_global(n);
     vm_obj r = s.get(0);
     display(p.ios().get_regular_stream(), r);
+    p.ios().get_regular_stream() << "\n";
     return p.env();
 }
 
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index d0d3717884..429047b05f 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/parray.h"
 #include "library/constants.h"
+#include "library/trace.h"
 #include "library/vm/vm.h"
 
 namespace lean {
@@ -538,8 +539,13 @@ if (is_constructor(obj)) {                              \
 
 #define InvokeGlobal(d)                                                 \
 if (d.is_builtin()) {                                                   \
-    d.get_fn()(*this);                                                  \
+    unsigned saved_bp = m_bp;                                           \
     unsigned sz = m_stack.size();                                       \
+    m_bp = sz - d.get_arity();                                          \
+    d.get_fn()(*this);                                                  \
+    lean_assert(m_stack.size() == sz + 1);                              \
+    m_bp = saved_bp;                                                    \
+    sz = m_stack.size();                                                \
     std::swap(m_stack[sz - d.get_arity() - 1], m_stack[sz - 1]);        \
     m_stack.resize(sz - d.get_arity());                                 \
     pc++;                                                               \
@@ -562,7 +568,6 @@ void vm_state::run() {
     lean_assert(m_code);
     unsigned init_call_stack_sz = m_call_stack.size();
     unsigned pc  = 0;
-
     while (true) {
       main_loop:
         vm_instr const & instr = m_code[pc];