From cb9bbea26eff003da7c4aa45a2ec4c2adcd4a9a8 Mon Sep 17 00:00:00 2001
From: Marek Trtik <marek.trtik@diffblue.com>
Date: Fri, 24 Nov 2017 15:19:28 +0000
Subject: [PATCH] Bugfix[byte_extract]: handling negative offsets by unknown
 bits.

---
 src/solvers/flattening/boolbv_byte_extract.cpp | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index 0cc2c46bd89..9782ef98aa9 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -98,16 +98,13 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   mp_integer index;
   if(!to_integer(offset, index))
   {
-    if(index<0)
-      throw "byte_extract flatting with negative offset: "+expr.pretty();
-
     mp_integer offset=index*byte_width;
 
-    std::size_t offset_i=integer2unsigned(offset);
+    long offset_i=offset.to_long();
 
-    for(std::size_t i=0; i<width; i++)
+    for(long i=0; i<(long)width; i++)
       // out of bounds?
-      if(offset<0 || offset_i+i>=op_bv.size())
+      if(offset<0 || offset_i+i>=(long)op_bv.size())
         bv[i]=prop.new_variable();
       else
         bv[i]=op_bv[offset_i+i];