From adff01bba417571e342cfbec4f1c5074b69d0323 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 Nov 2018 16:01:36 -0700
Subject: [PATCH] fix(library/vm/vm): handle `InvokeJP` at pc manipulation
 methods

---
 src/library/vm/vm.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index adb272071d..030c2d9699 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -577,6 +577,8 @@ unsigned vm_instr::get_num_pcs() const {
         return 2;
     case opcode::CasesN:
         return get_casesn_size();
+    case opcode::InvokeJP:
+        return 1;
     default:
         return 0;
     }
@@ -590,6 +592,8 @@ unsigned vm_instr::get_pc(unsigned i) const {
         return m_pc[i];
     case opcode::CasesN:
         return get_casesn_pc(i);
+    case opcode::InvokeJP:
+        return m_jp_pc;
     default:
         lean_unreachable();
     }
@@ -605,6 +609,9 @@ void vm_instr::set_pc(unsigned i, unsigned pc) {
     case opcode::CasesN:
         set_casesn_pc(i, pc);
         break;
+    case opcode::InvokeJP:
+        m_jp_pc = pc;
+        break;
     default:
         lean_unreachable();
     }