Incremental SMT2: fix shift extension for mismatched widths

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -24,6 +24,7 @@
 #include <functional>
 #include <numeric>
 #include <stack>
+#include <type_traits>
 
 /// Post order visitation is used in order to construct the the smt terms bottom
 /// upwards without using recursion to traverse the input `exprt`. Therefore
@@ -969,17 +970,23 @@ static smt_termt convert_to_smt_shift(
   const std::size_t second_width = second_bit_vector_sort->bit_width();
   if(first_width > second_width)
   {
+    // Shift distances are unsigned: always zero-extend the distance.
     return factory(
       first_operand,
-      extension_for_type(shift.op1().type())(first_width - second_width)(
+      smt_bit_vector_theoryt::zero_extend(first_width - second_width)(
         second_operand));
   }
   else if(first_width < second_width)
   {
-    const auto result = factory(
-      extension_for_type(shift.op0().type())(second_width - first_width)(
-        first_operand),
-      second_operand);
+    // The operand must be extended according to the shift kind, not
+    // its type signedness: ashr sign-extends (to shift copies of the
+    // MSB into the result), all others zero-extend.
+    const std::size_t ext = second_width - first_width;
+    const smt_termt extended_operand =
+      std::is_same<shiftt, ashr_exprt>::value
+        ? smt_termt{smt_bit_vector_theoryt::sign_extend(ext)(first_operand)}
+        : smt_termt{smt_bit_vector_theoryt::zero_extend(ext)(first_operand)};
+    const auto result = factory(extended_operand, second_operand);
     return smt_bit_vector_theoryt::extract(first_width - 1, 0)(result);
   }
   else

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1198,23 +1198,30 @@ TEST_CASE(
           symbol_exprt{"foo", make_type(32)},
           symbol_exprt{"bar", make_type(8)});
         INFO("Input expr: " + input.pretty(2, 0));
+        // Shift distances are always zero-extended, regardless of type.
         const smt_termt expected_result = make_shift_term(
           smt_identifier_termt{"foo", smt_bit_vector_sortt{32}},
-          make_extension(24)(
+          smt_bit_vector_theoryt::zero_extend(24)(
             smt_identifier_termt{"bar", smt_bit_vector_sortt{8}}));
         CHECK(test.convert(input) == expected_result);
       }
       SECTION("Wider right hand side")
       {
+        // The operand is extended by the shift kind: ashr sign-extends,
+        // lshr and shl zero-extend.
+        const smt_termt foo{
+          smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}};
+        const smt_termt extended_foo =
+          shift_description == "Arithmetic right shift."
+            ? smt_termt{smt_bit_vector_theoryt::sign_extend(24)(foo)}
+            : smt_termt{smt_bit_vector_theoryt::zero_extend(24)(foo)};
         const exprt input = make_shift_expr(
           symbol_exprt{"foo", make_type(8)},
           symbol_exprt{"bar", make_type(32)});
         INFO("Input expr: " + input.pretty(2, 0));
-        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}}));
+        const smt_termt expected_result = smt_bit_vector_theoryt::extract(
+          7, 0)(make_shift_term(
+          extended_foo, smt_identifier_termt{"bar", smt_bit_vector_sortt{32}}));
         CHECK(test.convert(input) == expected_result);
       }
     }