diff --git a/regression/smv/LTL/smv_ltlspec_H1.desc b/regression/smv/LTL/smv_ltlspec_H1.desc
new file mode 100644
index 000000000..c24dc4836
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_H1.desc
@@ -0,0 +1,8 @@
+CORE
+smv_ltlspec_H1.smv
+--bound 2
+^\[spec1\] H x != 5: FAILURE: property not supported by BMC engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/smv/LTL/smv_ltlspec_H1.smv b/regression/smv/LTL/smv_ltlspec_H1.smv
new file mode 100644
index 000000000..adc3a48fb
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_H1.smv
@@ -0,0 +1,14 @@
+MODULE main
+
+VAR x : 0..10;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x>=3 : 3;
+      TRUE: x+1;
+    esac;
+
+LTLSPEC H x != 5
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 2348f7870..d315890ab 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -23,6 +23,14 @@ IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)
 IREP_ID_ONE(smv_union)
+IREP_ID_ONE(smv_H)
+IREP_ID_ONE(smv_bounded_H)
+IREP_ID_ONE(smv_O)
+IREP_ID_ONE(smv_bounded_O)
+IREP_ID_ONE(smv_S)
+IREP_ID_ONE(smv_T)
+IREP_ID_ONE(smv_Y)
+IREP_ID_ONE(smv_Z)
 IREP_ID_ONE(sva_accept_on)
 IREP_ID_ONE(sva_reject_on)
 IREP_ID_ONE(sva_sync_accept_on)
diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp
index ce2c9b5c9..6318f5420 100644
--- a/src/smvlang/expr2smv.cpp
+++ b/src/smvlang/expr2smv.cpp
@@ -564,6 +564,26 @@ bool expr2smvt::convert(
       precedence = precedencet::TEMPORAL);
   }
 
+  else if(
+    src.id() == ID_smv_H || src.id() == ID_smv_O || src.id() == ID_smv_Y ||
+    src.id() == ID_smv_Z)
+  {
+    return convert_unary(
+      to_unary_expr(src),
+      dest,
+      std::string(src.id_string(), 4, std::string::npos) + " ",
+      precedence = precedencet::TEMPORAL);
+  }
+
+  else if(src.id() == ID_smv_bounded_H || src.id() == ID_smv_bounded_O)
+  {
+    return convert_unary(
+      to_unary_expr(src),
+      dest,
+      std::string(src.id_string(), 12, std::string::npos) + " ",
+      precedence = precedencet::TEMPORAL);
+  }
+
   else if(
     src.id() == ID_AU || src.id() == ID_EU || src.id() == ID_AR ||
     src.id() == ID_ER || src.id() == ID_U)
@@ -582,6 +602,15 @@ bool expr2smvt::convert(
       to_binary_expr(src), dest, "V", precedence = precedencet::TEMPORAL);
   }
 
+  else if(src.id() == ID_smv_S || src.id() == ID_smv_T)
+  {
+    return convert_binary(
+      to_binary_expr(src),
+      dest,
+      std::string(src.id_string(), 4, std::string::npos),
+      precedence = precedencet::TEMPORAL);
+  }
+
   else if(src.id() == ID_if)
     return convert_if(to_if_expr(src), dest, precedencet::IF);
 
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index 65bc2e17f..610bb80d1 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -284,7 +284,7 @@ static void new_module(YYSTYPE &module)
 %left  OR_Token
 %left  AND_Token
 %left  NOT_Token
-%left  EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token U_Token R_Token V_Token F_Token G_Token X_Token
+%left  EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token U_Token R_Token V_Token F_Token G_Token H_Token O_Token S_Token T_Token X_Token Y_Token Z_Token
 %left  EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
 %left  union_Token
 %left  IN_Token NOTIN_Token
@@ -704,6 +704,19 @@ term       : variable_name
            | term union_Token    term { binary($$, $1, ID_smv_union, $3); }
            | term IN_Token       term { binary($$, $1, ID_smv_setin, $3); }
            | term NOTIN_Token    term { binary($$, $1, ID_smv_setnotin, $3); }
+           /* LTL PAST */
+           | Y_Token term             { $$ = $1; stack_expr($$).id(ID_smv_Y); mto($$, $2); }
+           | Z_Token term             { $$ = $1; stack_expr($$).id(ID_smv_Z); mto($$, $2); }
+           | H_Token term             { $$ = $1; stack_expr($$).id(ID_smv_H); mto($$, $2); }
+           | H_Token bound term       { $$ = $1; stack_expr($$).id(ID_smv_bounded_H); mto($$, $3); }
+           | O_Token term             { $$ = $1; stack_expr($$).id(ID_smv_O); mto($$, $2); }
+           | O_Token bound term       { $$ = $1; stack_expr($$).id(ID_smv_bounded_O); mto($$, $3); }
+           | term S_Token term        { $$ = $2; stack_expr($$).id(ID_smv_S); mto($$, $1); mto($$, $3); }
+           | term T_Token term        { $$ = $2; stack_expr($$).id(ID_smv_T); mto($$, $1); mto($$, $3); }
+           ;
+
+bound:     '[' NUMBER_Token ',' NUMBER_Token ']'
+           { init($$); mto($$, $2); mto($$, $4); }
            ;
 
 formula_list:
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index a715ec59e..639646a13 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -986,7 +986,10 @@ void smv_typecheckt::typecheck_expr_rec(
     typecheck_expr_rec(op, mode);
     convert_expr_to(op, expr.type());
   }
-  else if(expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G)
+  else if(
+    expr.id() == ID_X || expr.id() == ID_F || expr.id() == ID_G ||
+    expr.id() == ID_smv_H || expr.id() == ID_smv_O || expr.id() == ID_smv_Y ||
+    expr.id() == ID_smv_Z)
   {
     if(mode != LTL)
       throw errort().with_location(expr.source_location())
@@ -1010,7 +1013,9 @@ void smv_typecheckt::typecheck_expr_rec(
     convert_expr_to(binary_expr.lhs(), expr.type());
     convert_expr_to(binary_expr.rhs(), expr.type());
   }
-  else if(expr.id() == ID_U || expr.id() == ID_R)
+  else if(
+    expr.id() == ID_U || expr.id() == ID_R || expr.id() == ID_smv_S ||
+    expr.id() == ID_smv_T)
   {
     if(mode != LTL)
       throw errort().with_location(expr.source_location())
diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
index b3c7e50fa..59b24a0e9 100644
--- a/src/temporal-logic/temporal_logic.cpp
+++ b/src/temporal-logic/temporal_logic.cpp
@@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 bool is_temporal_operator(const exprt &expr)
 {
   return is_CTL_operator(expr) || is_LTL_operator(expr) ||
-         is_SVA_operator(expr) || expr.id() == ID_A || expr.id() == ID_E;
+         is_LTL_past_operator(expr) || is_SVA_operator(expr) ||
+         expr.id() == ID_A || expr.id() == ID_E;
 }
 
 bool has_temporal_operator(const exprt &expr)
@@ -54,6 +55,14 @@ bool is_LTL_operator(const exprt &expr)
   return id == ID_G || id == ID_F || id == ID_X || id == ID_U || id == ID_R;
 }
 
+bool is_LTL_past_operator(const exprt &expr)
+{
+  auto id = expr.id();
+  return id == ID_smv_H || id == ID_smv_bounded_H || id == ID_smv_O ||
+         id == ID_smv_bounded_O || id == ID_smv_S || id == ID_smv_T ||
+         id == ID_smv_Y || id == ID_smv_Z;
+}
+
 bool is_LTL(const exprt &expr)
 {
   auto non_LTL_operator = [](const exprt &expr) {
@@ -63,6 +72,14 @@ bool is_LTL(const exprt &expr)
   return !has_subexpr(expr, non_LTL_operator);
 }
 
+bool is_LTL_past(const exprt &expr)
+{
+  auto non_LTL_past_operator = [](const exprt &expr)
+  { return is_temporal_operator(expr) && !is_LTL_past_operator(expr); };
+
+  return !has_subexpr(expr, non_LTL_past_operator);
+}
+
 bool is_SVA_sequence(const exprt &expr)
 {
   auto id = expr.id();
diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h
index f614633cb..1c03e4dc5 100644
--- a/src/temporal-logic/temporal_logic.h
+++ b/src/temporal-logic/temporal_logic.h
@@ -35,10 +35,17 @@ bool has_CTL_operator(const exprt &);
 /// Returns true iff the given expression is an LTL formula
 bool is_LTL(const exprt &);
 
+/// Returns true iff the given expression is an LTL past formula
+bool is_LTL_past(const exprt &);
+
 /// Returns true iff the given expression has an LTL operator
 /// as its root
 bool is_LTL_operator(const exprt &);
 
+/// Returns true iff the given expression has an LTL past operator
+/// as its root
+bool is_LTL_past_operator(const exprt &);
+
 /// Returns true iff the given expression is an SVA sequence expression
 bool is_SVA_sequence(const exprt &);