From a5e04d9dd178b2870b79776e1fbf1a858cdac49d Mon Sep 17 00:00:00 2001
From: Catalin Hritcu <catalin.hritcu@gmail.com>
Date: Sat, 5 Sep 2015 22:11:43 -0700
Subject: Fixed critical bug in 31 bit arithmetic of VM

ADDMULDIVINT31 was missing pops in some cases
---
 kernel/byterun/coq_interp.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0a121dc32..4937af77f 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1252,10 +1252,11 @@ value coq_interprete
         shiftby = uint32_of_value(accu);
         if (shiftby > 31) {
           if (shiftby < 62) {
-            *sp++;
+            sp++;
 	    accu = (value)((((*sp++)^1) << (shiftby - 31)) | 1);
           }
           else {
+            sp+=2;
             accu = (value)(1);
           }
 	}
-- 
cgit v1.2.3