SMT2: fix extractbit with non-const index

This fixes a constant literal in the encoding of extractbit for the case of
a non-const index.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -1812,9 +1812,10 @@ void smt2_convt::convert_expr(const exprt &expr)
       // the arguments of the shift need to have the same width
       out << "(bvlshr ";
       flatten2bv(extractbit_expr.src());
+      out << ' ';
       typecast_exprt tmp(extractbit_expr.index(), extractbit_expr.src().type());
       convert_expr(tmp);
-      out << ")) bin1)"; // bvlshr, extract, =
+      out << ")) #b1)"; // bvlshr, extract, =
     }
   }
   else if(expr.id()==ID_extractbits)