Fixed shift operator with size greater than first operand.

Author: Enrico Steffinlongo

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -164,6 +164,8 @@ extension_for_type(const typet &type)
     return smt_bit_vector_theoryt::sign_extend;
   if(can_cast_type<unsignedbv_typet>(type))
     return smt_bit_vector_theoryt::zero_extend;
+  if(can_cast_type<bv_typet>(type))
+    return smt_bit_vector_theoryt::zero_extend;
   UNREACHABLE;
 }
 
@@ -947,6 +949,9 @@ static smt_termt convert_to_smt_shift(
   INVARIANT(
     first_bit_vector_sort && second_bit_vector_sort,
     "Shift expressions are expected to have bit vector operands.");
+  INVARIANT(
+    shift.type() == shift.op0().type(),
+    "Shift expression type must be equals to first operand type.");
   const std::size_t first_width = first_bit_vector_sort->bit_width();
   const std::size_t second_width = second_bit_vector_sort->bit_width();
   if(first_width > second_width)
@@ -958,10 +963,11 @@ static smt_termt convert_to_smt_shift(
   }
   else if(first_width < second_width)
   {
-    return factory(
+    const auto result = factory(
       extension_for_type(shift.op0().type())(second_width - first_width)(
         first_operand),
       second_operand);
+    return smt_bit_vector_theoryt::extract(first_width - 1, 0)(result);
   }
   else
   {

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1209,10 +1209,11 @@ TEST_CASE(
           symbol_exprt{"foo", make_type(8)},
           symbol_exprt{"bar", make_type(32)});
         INFO("Input expr: " + input.pretty(2, 0));
-        const smt_termt expected_result = make_shift_term(
-          make_extension(24)(
-            smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}),
-          smt_identifier_termt{"bar", smt_bit_vector_sortt{32}});
+        const smt_termt expected_result =
+          smt_bit_vector_theoryt::extract(7, 0)(make_shift_term(
+            make_extension(24)(
+              smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}),
+            smt_identifier_termt{"bar", smt_bit_vector_sortt{32}}));
         CHECK(test.convert(input) == expected_result);
       }
     }