diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 5b7ab53c4ea..bab40d10016 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/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)