diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
index add14229d3f..c952506111f 100644
--- a/src/solvers/smt2/smt2_parser.cpp
+++ b/src/solvers/smt2/smt2_parser.cpp
@@ -1088,25 +1088,49 @@ void smt2_parsert::setup_expressions()
     return from_integer(ieee_floatt::ROUND_TO_EVEN, unsignedbv_typet(32));
   };
 
+  expressions["RNE"] = [] {
+    // we encode as 32-bit unsignedbv
+    return from_integer(ieee_floatt::ROUND_TO_EVEN, unsignedbv_typet(32));
+  };
+
   expressions["roundNearestTiesToAway"] = [this]() -> exprt {
     throw error("unsupported rounding mode");
   };
 
+  expressions["RNA"] = [this]() -> exprt {
+    throw error("unsupported rounding mode");
+  };
+
   expressions["roundTowardPositive"] = [] {
     // we encode as 32-bit unsignedbv
     return from_integer(ieee_floatt::ROUND_TO_PLUS_INF, unsignedbv_typet(32));
   };
 
+  expressions["RTP"] = [] {
+    // we encode as 32-bit unsignedbv
+    return from_integer(ieee_floatt::ROUND_TO_PLUS_INF, unsignedbv_typet(32));
+  };
+
   expressions["roundTowardNegative"] = [] {
     // we encode as 32-bit unsignedbv
     return from_integer(ieee_floatt::ROUND_TO_MINUS_INF, unsignedbv_typet(32));
   };
 
+  expressions["RTN"] = [] {
+    // we encode as 32-bit unsignedbv
+    return from_integer(ieee_floatt::ROUND_TO_MINUS_INF, unsignedbv_typet(32));
+  };
+
   expressions["roundTowardZero"] = [] {
     // we encode as 32-bit unsignedbv
     return from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32));
   };
 
+  expressions["RTZ"] = [] {
+    // we encode as 32-bit unsignedbv
+    return from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32));
+  };
+
   expressions["lambda"] = [this] { return lambda_expression(); };
   expressions["let"] = [this] { return let_expression(); };
   expressions["exists"] = [this] { return quantifier_expression(ID_exists); };