diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index 0151bd7fea..419d73200a 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -56,6 +56,8 @@ class vm_compiler_fn {
         name const & n = const_name(e);
         if (is_neutral_expr(e)) {
             emit(mk_sconstructor_instr(0));
+        } else if (is_unreachable_expr(e)) {
+            emit(mk_unreachable_instr());
         } else if (n == get_nat_zero_name()) {
             emit(mk_num_instr(mpz(0)));
         } else if (auto idx = is_internal_cnstr(e)) {
diff --git a/src/library/vm.cpp b/src/library/vm.cpp
index d2683c1914..177be7378e 100644
--- a/src/library/vm.cpp
+++ b/src/library/vm.cpp
@@ -144,6 +144,7 @@ void vm_instr::display(std::ostream & out, std::function<optional<name>(unsigned
     case opcode::SConstructor:  out << "scnstr " << m_cidx; break;
     case opcode::Constructor:   out << "cnstr " << m_cidx << " " << m_nfields; break;
     case opcode::Num:           out << "num " << *m_mpz; break;
+    case opcode::Unreachable:   out << "unreachable"; break;
     case opcode::Cases1:        out << "cases1"; break;
     case opcode::Cases2:        out << "cases2 " << m_pc; break;
     case opcode::CasesN:
@@ -218,6 +219,8 @@ vm_instr mk_ret_instr() { return vm_instr(opcode::Ret); }
 
 vm_instr mk_cases1_instr() { return vm_instr(opcode::Cases1); }
 
+vm_instr mk_unreachable_instr() { return vm_instr(opcode::Unreachable); }
+
 vm_instr mk_nat_cases_instr(unsigned pc) {
     vm_instr r(opcode::NatCases);
     r.m_pc = pc;
@@ -290,7 +293,7 @@ void vm_instr::copy_args(vm_instr const & i) {
     case opcode::Num:
         m_mpz = new mpz(*i.m_mpz);
         break;
-    case opcode::Ret: case opcode::Cases1:
+    case opcode::Ret: case opcode::Cases1: case opcode::Unreachable:
         break;
     }
 }
diff --git a/src/library/vm.h b/src/library/vm.h
index a8985b8f0a..a9491f0047 100644
--- a/src/library/vm.h
+++ b/src/library/vm.h
@@ -166,7 +166,7 @@ enum class opcode {
     Push, Ret, Drop, Goto,
     SConstructor, Constructor, Num,
     Cases1, Cases2, CasesN, NatCases, Proj,
-    Invoke, InvokeGlobal, Closure
+    Invoke, InvokeGlobal, Closure, Unreachable
 };
 
 /** \brief VM instructions */
@@ -194,7 +194,7 @@ class vm_instr {
         /* Num */
         mpz * m_mpz;
     };
-    /* Ret and Cases1 do not have arguments */
+    /* Ret, Cases1 and Unreachable do not have arguments */
     friend vm_instr mk_push_instr(unsigned idx);
     friend vm_instr mk_drop_instr(unsigned n);
     friend vm_instr mk_proj_instr(unsigned n);
@@ -204,6 +204,7 @@ class vm_instr {
     friend vm_instr mk_num_instr(mpz const & v);
     friend vm_instr mk_ret_instr();
     friend vm_instr mk_cases1_instr();
+    friend vm_instr mk_unreachable_instr();
     friend vm_instr mk_nat_cases_instr(unsigned pc);
     friend vm_instr mk_cases2_instr(unsigned pc);
     friend vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs);
@@ -297,6 +298,7 @@ vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields);
 vm_instr mk_num_instr(mpz const & v);
 vm_instr mk_ret_instr();
 vm_instr mk_cases1_instr();
+vm_instr mk_unreachable_instr();
 vm_instr mk_nat_cases_instr(unsigned pc);
 vm_instr mk_cases2_instr(unsigned pc);
 vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs);