diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp
index 235e84a88..e1f4fb086 100644
--- a/src/ebmc/bdd_engine.cpp
+++ b/src/ebmc/bdd_engine.cpp
@@ -15,7 +15,8 @@ Author: Daniel Kroening, daniel.kroening@inf.ethz.ch
 #include <ebmc/transition_system.h>
 #include <solvers/bdd/miniBDD/miniBDD.h>
 #include <solvers/sat/satcheck.h>
-#include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/ctl.h>
+#include <temporal-logic/ltl.h>
 #include <temporal-logic/temporal_logic.h>
 #include <trans-netlist/aig_prop.h>
 #include <trans-netlist/instantiate_netlist.h>
diff --git a/src/ebmc/live_signal.cpp b/src/ebmc/live_signal.cpp
index a0f8bc029..53e6dfc27 100644
--- a/src/ebmc/live_signal.cpp
+++ b/src/ebmc/live_signal.cpp
@@ -8,7 +8,7 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include "live_signal.h"
 
-#include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/ctl.h>
 #include <verilog/sva_expr.h>
 
 #include "transition_system.h"
diff --git a/src/ebmc/ranking_function.cpp b/src/ebmc/ranking_function.cpp
index 23a4b218c..d573d1605 100644
--- a/src/ebmc/ranking_function.cpp
+++ b/src/ebmc/ranking_function.cpp
@@ -15,7 +15,7 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include <langapi/language.h>
 #include <langapi/mode.h>
-#include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/ctl.h>
 #include <trans-word-level/instantiate_word_level.h>
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc
index 274c4712e..c6bebb8e1 100644
--- a/src/ic3/m1ain.cc
+++ b/src/ic3/m1ain.cc
@@ -18,7 +18,8 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <trans-netlist/netlist.h>
 #include <trans-netlist/trans_to_netlist.h>
 
-#include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/ctl.h>
+#include <temporal-logic/ltl.h>
 #include <temporal-logic/temporal_logic.h>
 
 #include <verilog/sva_expr.h>
diff --git a/src/temporal-logic/ctl.h b/src/temporal-logic/ctl.h
new file mode 100644
index 000000000..2bf7e2ef5
--- /dev/null
+++ b/src/temporal-logic/ctl.h
@@ -0,0 +1,238 @@
+/*******************************************************************\
+
+Module: CTL Temporal Operators
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_TEMPORAL_LOGIC_CTL_H
+#define CPROVER_TEMPORAL_LOGIC_CTL_H
+
+#include <util/std_expr.h>
+
+class AG_exprt : public unary_predicate_exprt
+{
+public:
+  explicit AG_exprt(exprt op) : unary_predicate_exprt(ID_AG, std::move(op))
+  {
+  }
+};
+
+static inline const AG_exprt &to_AG_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AG);
+  AG_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const AG_exprt &>(expr);
+}
+
+static inline AG_exprt &to_AG_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AG);
+  AG_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<AG_exprt &>(expr);
+}
+
+class AF_exprt : public unary_predicate_exprt
+{
+public:
+  explicit AF_exprt(exprt op) : unary_predicate_exprt(ID_AF, std::move(op))
+  {
+  }
+};
+
+static inline const AF_exprt &to_AF_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AF);
+  AF_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const AF_exprt &>(expr);
+}
+
+static inline AF_exprt &to_AF_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AF);
+  AF_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<AF_exprt &>(expr);
+}
+
+class EG_exprt : public unary_predicate_exprt
+{
+public:
+  explicit EG_exprt(exprt op) : unary_predicate_exprt(ID_EG, std::move(op))
+  {
+  }
+};
+
+static inline const EG_exprt &to_EG_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_EG);
+  EG_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const EG_exprt &>(expr);
+}
+
+static inline EG_exprt &to_EG_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_EG);
+  EG_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<EG_exprt &>(expr);
+}
+
+class EF_exprt : public unary_predicate_exprt
+{
+public:
+  explicit EF_exprt(exprt op) : unary_predicate_exprt(ID_EF, std::move(op))
+  {
+  }
+};
+
+static inline const EF_exprt &to_EF_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_EF);
+  EF_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const EF_exprt &>(expr);
+}
+
+static inline EF_exprt &to_EF_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_EF);
+  EF_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<EF_exprt &>(expr);
+}
+
+class EU_exprt : public binary_predicate_exprt
+{
+public:
+  explicit EU_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_EU, std::move(op1))
+  {
+  }
+};
+
+static inline const EU_exprt &to_EU_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_EU);
+  EU_exprt::check(expr);
+  return static_cast<const EU_exprt &>(expr);
+}
+
+static inline EU_exprt &to_EU_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_EU);
+  EU_exprt::check(expr);
+  return static_cast<EU_exprt &>(expr);
+}
+
+class AU_exprt : public binary_predicate_exprt
+{
+public:
+  explicit AU_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_AU, std::move(op1))
+  {
+  }
+};
+
+static inline const AU_exprt &to_AU_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AU);
+  AU_exprt::check(expr);
+  return static_cast<const AU_exprt &>(expr);
+}
+
+static inline AU_exprt &to_AU_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AU);
+  AU_exprt::check(expr);
+  return static_cast<AU_exprt &>(expr);
+}
+
+class ER_exprt : public binary_predicate_exprt
+{
+public:
+  explicit ER_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_ER, std::move(op1))
+  {
+  }
+};
+
+static inline const ER_exprt &to_ER_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_ER);
+  ER_exprt::check(expr);
+  return static_cast<const ER_exprt &>(expr);
+}
+
+static inline ER_exprt &to_ER_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_ER);
+  ER_exprt::check(expr);
+  return static_cast<ER_exprt &>(expr);
+}
+
+class AR_exprt : public binary_predicate_exprt
+{
+public:
+  explicit AR_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_AR, std::move(op1))
+  {
+  }
+};
+
+static inline const AR_exprt &to_AR_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AR);
+  AR_exprt::check(expr);
+  return static_cast<const AR_exprt &>(expr);
+}
+
+static inline AR_exprt &to_AR_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AR);
+  AR_exprt::check(expr);
+  return static_cast<AR_exprt &>(expr);
+}
+
+class AX_exprt : public unary_predicate_exprt
+{
+public:
+  explicit AX_exprt(exprt op) : unary_predicate_exprt(ID_AX, std::move(op))
+  {
+  }
+};
+
+static inline const AX_exprt &to_AX_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AX);
+  AX_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const AX_exprt &>(expr);
+}
+
+static inline AX_exprt &to_AX_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_AX);
+  AX_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<AX_exprt &>(expr);
+}
+
+class EX_exprt : public unary_predicate_exprt
+{
+public:
+  explicit EX_exprt(exprt op) : unary_predicate_exprt(ID_EX, std::move(op))
+  {
+  }
+};
+
+static inline const EX_exprt &to_EX_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_EX);
+  EX_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const EX_exprt &>(expr);
+}
+
+static inline EX_exprt &to_EX_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_EX);
+  EX_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<EX_exprt &>(expr);
+}
+
+#endif
diff --git a/src/temporal-logic/ltl.h b/src/temporal-logic/ltl.h
new file mode 100644
index 000000000..e714dbee1
--- /dev/null
+++ b/src/temporal-logic/ltl.h
@@ -0,0 +1,176 @@
+/*******************************************************************\
+
+Module: LTL Temporal Operators
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_TEMPORAL_LOGIC_LTL_H
+#define CPROVER_TEMPORAL_LOGIC_LTL_H
+
+#include <util/std_expr.h>
+
+class F_exprt : public unary_predicate_exprt
+{
+public:
+  explicit F_exprt(exprt op) : unary_predicate_exprt(ID_F, std::move(op))
+  {
+  }
+};
+
+static inline const F_exprt &to_F_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_F);
+  F_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const F_exprt &>(expr);
+}
+
+static inline F_exprt &to_F_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_F);
+  F_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<F_exprt &>(expr);
+}
+
+class G_exprt : public unary_predicate_exprt
+{
+public:
+  explicit G_exprt(exprt op) : unary_predicate_exprt(ID_G, std::move(op))
+  {
+  }
+};
+
+static inline const G_exprt &to_G_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_G);
+  G_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const G_exprt &>(expr);
+}
+
+static inline G_exprt &to_G_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_G);
+  G_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<G_exprt &>(expr);
+}
+
+/// standard (strong) LTL until, i.e.,
+/// the rhs must become true eventually
+class U_exprt : public binary_predicate_exprt
+{
+public:
+  explicit U_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_U, std::move(op1))
+  {
+  }
+};
+
+static inline const U_exprt &to_U_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_U);
+  U_exprt::check(expr);
+  return static_cast<const U_exprt &>(expr);
+}
+
+static inline U_exprt &to_U_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_U);
+  U_exprt::check(expr);
+  return static_cast<U_exprt &>(expr);
+}
+
+/// weak LTL until, i.e.,
+/// the rhs is not required to become true eventually
+class weak_U_exprt : public binary_predicate_exprt
+{
+public:
+  explicit weak_U_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_weak_U, std::move(op1))
+  {
+  }
+};
+
+static inline const weak_U_exprt &to_weak_U_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_weak_U);
+  weak_U_exprt::check(expr);
+  return static_cast<const weak_U_exprt &>(expr);
+}
+
+static inline weak_U_exprt &to_weak_U_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_weak_U);
+  weak_U_exprt::check(expr);
+  return static_cast<weak_U_exprt &>(expr);
+}
+
+class R_exprt : public binary_predicate_exprt
+{
+public:
+  explicit R_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_R, std::move(op1))
+  {
+  }
+};
+
+static inline const R_exprt &to_R_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_R);
+  R_exprt::check(expr);
+  return static_cast<const R_exprt &>(expr);
+}
+
+static inline R_exprt &to_R_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_R);
+  R_exprt::check(expr);
+  return static_cast<R_exprt &>(expr);
+}
+
+class strong_R_exprt : public binary_predicate_exprt
+{
+public:
+  explicit strong_R_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_strong_R, std::move(op1))
+  {
+  }
+};
+
+static inline const strong_R_exprt &to_strong_R_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_strong_R);
+  strong_R_exprt::check(expr);
+  return static_cast<const strong_R_exprt &>(expr);
+}
+
+static inline strong_R_exprt &to_strong_R_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_strong_R);
+  strong_R_exprt::check(expr);
+  return static_cast<strong_R_exprt &>(expr);
+}
+
+class X_exprt : public unary_predicate_exprt
+{
+public:
+  explicit X_exprt(exprt op) : unary_predicate_exprt(ID_X, std::move(op))
+  {
+  }
+};
+
+static inline const X_exprt &to_X_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_X);
+  X_exprt::check(expr);
+  return static_cast<const X_exprt &>(expr);
+}
+
+static inline X_exprt &to_X_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_X);
+  X_exprt::check(expr);
+  return static_cast<X_exprt &>(expr);
+}
+
+#endif
diff --git a/src/temporal-logic/nnf.cpp b/src/temporal-logic/nnf.cpp
index 4a2f6f007..a02481277 100644
--- a/src/temporal-logic/nnf.cpp
+++ b/src/temporal-logic/nnf.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include <verilog/sva_expr.h>
 
+#include "ltl.h"
 #include "temporal_expr.h"
 
 std::optional<exprt> negate_property_node(const exprt &expr)
diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
index 0442a1788..14704f289 100644
--- a/src/temporal-logic/normalize_property.cpp
+++ b/src/temporal-logic/normalize_property.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include <verilog/sva_expr.h>
 
+#include "ltl.h"
 #include "nnf.h"
 #include "temporal_expr.h"
 #include "temporal_logic.h"
diff --git a/src/temporal-logic/temporal_expr.h b/src/temporal-logic/temporal_expr.h
index 368b58ad4..2d3fc014b 100644
--- a/src/temporal-logic/temporal_expr.h
+++ b/src/temporal-logic/temporal_expr.h
@@ -11,326 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_expr.h>
 
-class AG_exprt : public unary_predicate_exprt
-{
-public:
-  explicit AG_exprt(exprt op) : unary_predicate_exprt(ID_AG, std::move(op))
-  {
-  }
-};
-
-static inline const AG_exprt &to_AG_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AG);
-  AG_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const AG_exprt &>(expr);
-}
-
-static inline AG_exprt &to_AG_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AG);
-  AG_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<AG_exprt &>(expr);
-}
-
-class AF_exprt : public unary_predicate_exprt
-{
-public:
-  explicit AF_exprt(exprt op) : unary_predicate_exprt(ID_AF, std::move(op))
-  {
-  }
-};
-
-static inline const AF_exprt &to_AF_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AF);
-  AF_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const AF_exprt &>(expr);
-}
-
-static inline AF_exprt &to_AF_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AF);
-  AF_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<AF_exprt &>(expr);
-}
-
-class EG_exprt : public unary_predicate_exprt
-{
-public:
-  explicit EG_exprt(exprt op) : unary_predicate_exprt(ID_EG, std::move(op))
-  {
-  }
-};
-
-static inline const EG_exprt &to_EG_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_EG);
-  EG_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const EG_exprt &>(expr);
-}
-
-static inline EG_exprt &to_EG_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_EG);
-  EG_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<EG_exprt &>(expr);
-}
-
-class EF_exprt : public unary_predicate_exprt
-{
-public:
-  explicit EF_exprt(exprt op) : unary_predicate_exprt(ID_EF, std::move(op))
-  {
-  }
-};
-
-static inline const EF_exprt &to_EF_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_EF);
-  EF_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const EF_exprt &>(expr);
-}
-
-static inline EF_exprt &to_EF_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_EF);
-  EF_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<EF_exprt &>(expr);
-}
-
-class F_exprt : public unary_predicate_exprt
-{
-public:
-  explicit F_exprt(exprt op) : unary_predicate_exprt(ID_F, std::move(op))
-  {
-  }
-};
-
-static inline const F_exprt &to_F_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_F);
-  F_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const F_exprt &>(expr);
-}
-
-static inline F_exprt &to_F_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_F);
-  F_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<F_exprt &>(expr);
-}
-
-class G_exprt : public unary_predicate_exprt
-{
-public:
-  explicit G_exprt(exprt op) : unary_predicate_exprt(ID_G, std::move(op))
-  {
-  }
-};
-
-static inline const G_exprt &to_G_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_G);
-  G_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const G_exprt &>(expr);
-}
-
-static inline G_exprt &to_G_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_G);
-  G_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<G_exprt &>(expr);
-}
-
-/// standard (strong) LTL until, i.e.,
-/// the rhs must become true eventually
-class U_exprt : public binary_predicate_exprt
-{
-public:
-  explicit U_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_U, std::move(op1))
-  {
-  }
-};
-
-static inline const U_exprt &to_U_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_U);
-  U_exprt::check(expr);
-  return static_cast<const U_exprt &>(expr);
-}
-
-static inline U_exprt &to_U_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_U);
-  U_exprt::check(expr);
-  return static_cast<U_exprt &>(expr);
-}
-
-/// weak LTL until, i.e.,
-/// the rhs is not required to become true eventually
-class weak_U_exprt : public binary_predicate_exprt
-{
-public:
-  explicit weak_U_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_weak_U, std::move(op1))
-  {
-  }
-};
-
-static inline const weak_U_exprt &to_weak_U_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_weak_U);
-  weak_U_exprt::check(expr);
-  return static_cast<const weak_U_exprt &>(expr);
-}
-
-static inline weak_U_exprt &to_weak_U_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_weak_U);
-  weak_U_exprt::check(expr);
-  return static_cast<weak_U_exprt &>(expr);
-}
-
-class EU_exprt : public binary_predicate_exprt
-{
-public:
-  explicit EU_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_EU, std::move(op1))
-  {
-  }
-};
-
-static inline const EU_exprt &to_EU_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_EU);
-  EU_exprt::check(expr);
-  return static_cast<const EU_exprt &>(expr);
-}
-
-static inline EU_exprt &to_EU_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_EU);
-  EU_exprt::check(expr);
-  return static_cast<EU_exprt &>(expr);
-}
-
-class AU_exprt : public binary_predicate_exprt
-{
-public:
-  explicit AU_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_AU, std::move(op1))
-  {
-  }
-};
-
-static inline const AU_exprt &to_AU_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AU);
-  AU_exprt::check(expr);
-  return static_cast<const AU_exprt &>(expr);
-}
-
-static inline AU_exprt &to_AU_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AU);
-  AU_exprt::check(expr);
-  return static_cast<AU_exprt &>(expr);
-}
-
-class R_exprt : public binary_predicate_exprt
-{
-public:
-  explicit R_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_R, std::move(op1))
-  {
-  }
-};
-
-static inline const R_exprt &to_R_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_R);
-  R_exprt::check(expr);
-  return static_cast<const R_exprt &>(expr);
-}
-
-static inline R_exprt &to_R_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_R);
-  R_exprt::check(expr);
-  return static_cast<R_exprt &>(expr);
-}
-
-class strong_R_exprt : public binary_predicate_exprt
-{
-public:
-  explicit strong_R_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_strong_R, std::move(op1))
-  {
-  }
-};
-
-static inline const strong_R_exprt &to_strong_R_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_strong_R);
-  strong_R_exprt::check(expr);
-  return static_cast<const strong_R_exprt &>(expr);
-}
-
-static inline strong_R_exprt &to_strong_R_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_strong_R);
-  strong_R_exprt::check(expr);
-  return static_cast<strong_R_exprt &>(expr);
-}
-
-class ER_exprt : public binary_predicate_exprt
-{
-public:
-  explicit ER_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_ER, std::move(op1))
-  {
-  }
-};
-
-static inline const ER_exprt &to_ER_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_ER);
-  R_exprt::check(expr);
-  return static_cast<const ER_exprt &>(expr);
-}
-
-static inline ER_exprt &to_ER_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_ER);
-  R_exprt::check(expr);
-  return static_cast<ER_exprt &>(expr);
-}
-
-class AR_exprt : public binary_predicate_exprt
-{
-public:
-  explicit AR_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_AR, std::move(op1))
-  {
-  }
-};
-
-static inline const AR_exprt &to_AR_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AR);
-  R_exprt::check(expr);
-  return static_cast<const AR_exprt &>(expr);
-}
-
-static inline AR_exprt &to_AR_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AR);
-  R_exprt::check(expr);
-  return static_cast<AR_exprt &>(expr);
-}
-
 class E_exprt : public binary_predicate_exprt
 {
 public:
@@ -377,70 +57,4 @@ static inline A_exprt &to_A_expr(exprt &expr)
   return static_cast<A_exprt &>(expr);
 }
 
-class AX_exprt : public unary_predicate_exprt
-{
-public:
-  explicit AX_exprt(exprt op) : unary_predicate_exprt(ID_AX, std::move(op))
-  {
-  }
-};
-
-static inline const AX_exprt &to_AX_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AX);
-  AX_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const AX_exprt &>(expr);
-}
-
-static inline AX_exprt &to_AX_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_AX);
-  AX_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<AX_exprt &>(expr);
-}
-
-class EX_exprt : public unary_predicate_exprt
-{
-public:
-  explicit EX_exprt(exprt op) : unary_predicate_exprt(ID_EX, std::move(op))
-  {
-  }
-};
-
-static inline const EX_exprt &to_EX_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_EX);
-  EX_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<const EX_exprt &>(expr);
-}
-
-static inline EX_exprt &to_EX_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_EX);
-  EX_exprt::check(expr, validation_modet::INVARIANT);
-  return static_cast<EX_exprt &>(expr);
-}
-
-class X_exprt : public unary_predicate_exprt
-{
-public:
-  explicit X_exprt(exprt op) : unary_predicate_exprt(ID_X, std::move(op))
-  {
-  }
-};
-
-static inline const X_exprt &to_X_expr(const exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_X);
-  X_exprt::check(expr);
-  return static_cast<const X_exprt &>(expr);
-}
-
-static inline X_exprt &to_X_expr(exprt &expr)
-{
-  PRECONDITION(expr.id() == ID_X);
-  X_exprt::check(expr);
-  return static_cast<X_exprt &>(expr);
-}
-
 #endif
diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp
index a59b33f2d..3cf39dea1 100644
--- a/src/trans-netlist/trans_to_netlist.cpp
+++ b/src/trans-netlist/trans_to_netlist.cpp
@@ -17,7 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 
 #include <solvers/flattening/boolbv_width.h>
-#include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/ctl.h>
+#include <temporal-logic/ltl.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
diff --git a/src/trans-netlist/unwind_netlist.cpp b/src/trans-netlist/unwind_netlist.cpp
index 55e9dcd39..d52c067c8 100644
--- a/src/trans-netlist/unwind_netlist.cpp
+++ b/src/trans-netlist/unwind_netlist.cpp
@@ -11,7 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ebmc_util.h>
 #include <util/expr_util.h>
 
-#include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/ctl.h>
+#include <temporal-logic/ltl.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index 991bc4229..1d4b4164c 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -17,8 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/symbol_table.h>
 
 #include <ebmc/ebmc_error.h>
+#include <temporal-logic/ctl.h>
+#include <temporal-logic/ltl.h>
 #include <temporal-logic/nnf.h>
-#include <temporal-logic/temporal_expr.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
diff --git a/src/vhdl/vhdl_synthesis.cpp b/src/vhdl/vhdl_synthesis.cpp
index 4fd04a316..b7a23a0a9 100644
--- a/src/vhdl/vhdl_synthesis.cpp
+++ b/src/vhdl/vhdl_synthesis.cpp
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_expr.h>
 #include <util/std_expr.h>
 
-#include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/ctl.h>
 
 /*******************************************************************\