Extend unit test of extract_bits conversion with integer bounds

Because instances of this expression are constructed using integer
bounds rather than bit vector bounds, as part of the left shift overflow
checks.

Author: thomasspriggs

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -920,20 +920,34 @@ TEST_CASE(
   "[core][smt2_incremental]")
 {
   const typet operand_type = unsignedbv_typet{8};
-  const exprt input = extractbits_exprt{
-    symbol_exprt{"foo", operand_type},
-    from_integer(4, operand_type),
-    from_integer(2, operand_type),
-    unsignedbv_typet{3}};
+  std::string description;
+  exprt input;
+  using rowt = std::pair<std::string, exprt>;
+  std::tie(description, input) = GENERATE_REF(
+    rowt{
+      "Bit vector typed bounds",
+      extractbits_exprt{
+        symbol_exprt{"foo", operand_type},
+        from_integer(4, operand_type),
+        from_integer(2, operand_type),
+        unsignedbv_typet{3}}},
+    rowt{
+      "Constant integer bounds",
+      extractbits_exprt{
+        symbol_exprt{"foo", operand_type}, 4, 2, unsignedbv_typet{3}}});
   const smt_termt expected_result = smt_bit_vector_theoryt::extract(4, 2)(
     smt_identifier_termt{"foo", smt_bit_vector_sortt{8}});
-  CHECK(convert_expr_to_smt(input) == expected_result);
-  const cbmc_invariants_should_throwt invariants_throw;
-  CHECK_THROWS(convert_expr_to_smt(extractbits_exprt{
-    symbol_exprt{"foo", operand_type},
-    symbol_exprt{"bar", operand_type},
-    symbol_exprt{"bar", operand_type},
-    unsignedbv_typet{3}}));
+  SECTION(description)
+  {
+    INFO("Input expression - " + input.pretty(1, 0));
+    CHECK(convert_expr_to_smt(input) == expected_result);
+    const cbmc_invariants_should_throwt invariants_throw;
+    CHECK_THROWS(convert_expr_to_smt(extractbits_exprt{
+      symbol_exprt{"foo", operand_type},
+      symbol_exprt{"bar", operand_type},
+      symbol_exprt{"bar", operand_type},
+      unsignedbv_typet{3}}));
+  }
 }
 
 TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")