From ced436a707991a3e7018e0380bbbc2fc039c360b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 11 Jul 2017 13:35:51 +0100 Subject: [PATCH] fix(library/vm/vm_nat): fix VM definition of nat.shiftr fixes #1723 --- src/library/vm/vm_nat.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/vm/vm_nat.cpp b/src/library/vm/vm_nat.cpp index fd335c9fd6..e9d8f588cd 100644 --- a/src/library/vm/vm_nat.cpp +++ b/src/library/vm/vm_nat.cpp @@ -175,7 +175,8 @@ vm_obj nat_shiftl(vm_obj const & a1, vm_obj const & a2) { vm_obj nat_shiftr(vm_obj const & a1, vm_obj const & a2) { if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_nat(cidx(a1) >> cidx(a2)); + int v2 = cidx(a2); + return v2 < 32 ? mk_vm_nat(cidx(a1) >> v2) : mk_vm_simple(0); } else { mpz v1 = to_mpz1(a1); div2k(v1, v1, to_unsigned(a2));