Merge pull request #3548 from diffblue/smt2_sign_extend

smt2 parser: fix sign extension

Author: Daniel Kroening

scripts/delete_failing_smt2_solver_tests

@@ -9,7 +9,6 @@ rm Empty_struct1/test.desc
 rm Endianness4/test.desc
 rm Endianness6/test.desc
 rm Endianness7/test.desc
-rm Fixedbv8/test.desc
 rm Float-div2/test.desc
 rm Float-div3/test.desc
 rm Float-no-simp1/test.desc
@@ -67,7 +66,6 @@ rm Quantifiers-not-exists/test.desc
 rm Quantifiers-two-dimension-array/test.desc
 rm Quantifiers-type/test.desc
 rm Struct_Bytewise2/test.desc
-rm Typecast1/test.desc
 rm Union_Initialization1/test.desc
 rm address_space_size_limit1/test.desc
 rm address_space_size_limit3/test.desc

src/solvers/smt2/smt2_parser.cpp

@@ -780,12 +780,17 @@ exprt smt2_parsert::function_application()
           }
           else if(id=="sign_extend")
           {
-            auto width=to_unsignedbv_type(op[0].type()).get_width();
-            signedbv_typet signed_type(width+index);
-            unsignedbv_typet unsigned_type(width+index);
+            // we first convert to a signed type of the original width,
+            // then extend to the new width, and then go to unsigned
+            const auto width = to_unsignedbv_type(op[0].type()).get_width();
+            const signedbv_typet small_signed_type(width);
+            const signedbv_typet large_signed_type(width + index);
+            const unsignedbv_typet unsigned_type(width + index);
 
             return typecast_exprt(
-              typecast_exprt(op[0], signed_type), unsigned_type);
+              typecast_exprt(
+                typecast_exprt(op[0], small_signed_type), large_signed_type),
+              unsigned_type);
           }
           else if(id=="zero_extend")
           {