diff --git a/src/ebmc/completeness_threshold.cpp b/src/ebmc/completeness_threshold.cpp
index 0238dd68..d029dade 100644
--- a/src/ebmc/completeness_threshold.cpp
+++ b/src/ebmc/completeness_threshold.cpp
@@ -68,10 +68,18 @@ bool has_low_completeness_threshold(const exprt &expr)
     expr.id() == ID_sva_implicit_strong || expr.id() == ID_sva_implicit_weak)
   {
     auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
-    if(!is_SVA_sequence_operator(sequence))
-      return true;
-    else
-      return false;
+    return has_low_completeness_threshold(sequence);
+  }
+  else if(expr.id() == ID_sva_boolean)
+  {
+    return true;
+  }
+  else if(expr.id() == ID_sva_or || expr.id() == ID_sva_and)
+  {
+    for(auto &op : expr.operands())
+      if(!has_low_completeness_threshold(op))
+        return false;
+    return true;
   }
   else if(expr.id() == ID_sva_sequence_property)
   {
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index d7152df8..5b35ef56 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -45,6 +45,7 @@ IREP_ID_ONE(smv_EBG)
 IREP_ID_ONE(smv_ABG)
 IREP_ID_ONE(smv_ABU)
 IREP_ID_ONE(smv_EBU)
+IREP_ID_ONE(sva_boolean)
 IREP_ID_ONE(sva_accept_on)
 IREP_ID_ONE(sva_reject_on)
 IREP_ID_ONE(sva_sync_accept_on)
@@ -139,6 +140,7 @@ IREP_ID_ONE(verilog_null)
 IREP_ID_ONE(verilog_event)
 IREP_ID_ONE(verilog_event_trigger)
 IREP_ID_ONE(verilog_string)
+IREP_ID_ONE(verilog_sva_property)
 IREP_ID_ONE(verilog_sva_sequence)
 IREP_ID_ONE(reg)
 IREP_ID_ONE(macromodule)
diff --git a/src/temporal-logic/nnf.cpp b/src/temporal-logic/nnf.cpp
index 74eecc48..db29e1c2 100644
--- a/src/temporal-logic/nnf.cpp
+++ b/src/temporal-logic/nnf.cpp
@@ -149,6 +149,24 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     return sva_non_overlapped_implication_exprt{
       followed_by.antecedent(), not_b};
   }
+  else if(expr.id() == ID_sva_overlapped_implication)
+  {
+    // 1800 2017 16.12.9
+    // !(a |-> b)   --->   a #-# !b
+    auto &implication = to_sva_implication_base_expr(expr);
+    auto not_b = not_exprt{implication.consequent()};
+    return sva_followed_by_exprt{
+      implication.antecedent(), ID_sva_overlapped_followed_by, not_b};
+  }
+  else if(expr.id() == ID_sva_non_overlapped_implication)
+  {
+    // 1800 2017 16.12.9
+    // !(a |=> b)   --->   a #=# !b
+    auto &implication = to_sva_implication_base_expr(expr);
+    auto not_b = not_exprt{implication.consequent()};
+    return sva_followed_by_exprt{
+      implication.antecedent(), ID_sva_nonoverlapped_followed_by, not_b};
+  }
   else
     return {};
 }
diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
index 4d972345..f6945f11 100644
--- a/src/temporal-logic/normalize_property.cpp
+++ b/src/temporal-logic/normalize_property.cpp
@@ -23,12 +23,26 @@ Author: Daniel Kroening, dkr@amazon.com
 exprt normalize_pre_sva_non_overlapped_implication(
   sva_non_overlapped_implication_exprt expr)
 {
-  // Same as a->always[1:1] b if lhs is not a sequence.
-  if(!is_SVA_sequence_operator(expr.lhs()))
+  // a|=>b is the same as a->always[1:1] b if lhs is not a proper sequence.
+  if(expr.lhs().id() == ID_sva_boolean)
   {
+    const auto &lhs_cond = to_sva_boolean_expr(expr.lhs()).op();
     auto one = natural_typet{}.one_expr();
     return or_exprt{
-      not_exprt{expr.lhs()}, sva_ranged_always_exprt{one, one, expr.rhs()}};
+      not_exprt{lhs_cond}, sva_ranged_always_exprt{one, one, expr.rhs()}};
+  }
+  else
+    return std::move(expr);
+}
+
+exprt normalize_pre_sva_overlapped_implication(
+  sva_overlapped_implication_exprt expr)
+{
+  // a|->b is the same as a->b if lhs is not a proper sequence.
+  if(expr.lhs().id() == ID_sva_boolean)
+  {
+    const auto &lhs_cond = to_sva_boolean_expr(expr.lhs()).op();
+    return implies_exprt{lhs_cond, expr.rhs()};
   }
   else
     return std::move(expr);
@@ -42,6 +56,11 @@ exprt normalize_property_rec(exprt expr)
     expr = normalize_pre_sva_non_overlapped_implication(
       to_sva_non_overlapped_implication_expr(expr));
   }
+  else if(expr.id() == ID_sva_overlapped_implication)
+  {
+    expr = normalize_pre_sva_overlapped_implication(
+      to_sva_overlapped_implication_expr(expr));
+  }
   else if(expr.id() == ID_sva_nexttime)
   {
     auto one = natural_typet{}.one_expr();
@@ -86,7 +105,7 @@ exprt normalize_property(exprt expr)
 {
   // top-level only
   if(expr.id() == ID_sva_cover)
-    expr = sva_always_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
+    expr = sva_always_exprt{sva_not_exprt{to_sva_cover_expr(expr).op()}};
 
   expr = trivial_sva(expr);
 
diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h
index 56085d76..23e29a08 100644
--- a/src/temporal-logic/normalize_property.h
+++ b/src/temporal-logic/normalize_property.h
@@ -13,15 +13,14 @@ Author: Daniel Kroening, dkr@amazon.com
 
 /// This applies the following rewrites:
 ///
-/// cover(φ) --> G¬φ
-///
 /// -----Propositional-----
 /// ¬(a ∨ b) --> ¬a ∧ ¬b
 /// ¬(a ∧ b) --> ¬a ∨ ¬b
 /// (a -> b) --> ¬a ∨ b
 ///
 /// -----SVA-----
-/// sva_non_overlapped_implication --> ¬a ∨ always[1:1] b   if a is not an SVA sequence
+/// a|=>b --> ¬a ∨ always[1:1] b   if a is not an SVA sequence
+/// a|->b --> a⇒b                  if a is not an SVA sequence
 /// sva_nexttime φ --> sva_always[1:1] φ
 /// sva_nexttime[i] φ --> sva_always[i:i] φ
 /// sva_s_nexttime φ --> sva_always[1:1] φ
diff --git a/src/temporal-logic/sva_to_ltl.cpp b/src/temporal-logic/sva_to_ltl.cpp
index 9b993e40..21df28ce 100644
--- a/src/temporal-logic/sva_to_ltl.cpp
+++ b/src/temporal-logic/sva_to_ltl.cpp
@@ -42,10 +42,10 @@ struct ltl_sequence_matcht
 
 std::vector<ltl_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
 {
-  if(!is_SVA_sequence_operator(sequence))
+  if(sequence.id() == ID_sva_boolean)
   {
     // atomic proposition
-    return {{sequence, 1}};
+    return {{to_sva_boolean_expr(sequence).op(), 1}};
   }
   else if(sequence.id() == ID_sva_sequence_concatenation)
   {
diff --git a/src/temporal-logic/trivial_sva.cpp b/src/temporal-logic/trivial_sva.cpp
index ba1d164d..d0a43ff3 100644
--- a/src/temporal-logic/trivial_sva.cpp
+++ b/src/temporal-logic/trivial_sva.cpp
@@ -12,12 +12,10 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include "temporal_logic.h"
 
-static std::optional<exprt> is_state_formula(const exprt &expr)
+static std::optional<exprt> is_state_predicate(const exprt &expr)
 {
-  if(expr.id() == ID_typecast && expr.type().id() == ID_verilog_sva_sequence)
-    return to_typecast_expr(expr).op();
-  else if(expr.type().id() == ID_bool)
-    return expr;
+  if(expr.id() == ID_sva_boolean)
+    return to_sva_boolean_expr(expr).op();
   else
     return {};
 }
@@ -30,8 +28,8 @@ exprt trivial_sva(exprt expr)
     // Same as regular implication if lhs and rhs are not sequences.
     auto &sva_implication = to_sva_overlapped_implication_expr(expr);
 
-    auto lhs = is_state_formula(sva_implication.lhs());
-    auto rhs = is_state_formula(sva_implication.rhs());
+    auto lhs = is_state_predicate(sva_implication.lhs());
+    auto rhs = is_state_predicate(sva_implication.rhs());
 
     if(lhs.has_value() && rhs.has_value())
       expr = implies_exprt{*lhs, *rhs};
@@ -50,27 +48,43 @@ exprt trivial_sva(exprt expr)
   {
     auto &sva_and = to_sva_and_expr(expr);
 
-    // Same as a ∧ b if the expression is not a sequence.
-    auto lhs = is_state_formula(sva_and.lhs());
-    auto rhs = is_state_formula(sva_and.rhs());
-
-    if(lhs.has_value() && rhs.has_value())
-      expr = and_exprt{*lhs, *rhs};
+    // can be sequence or property
+    if(expr.type().id() == ID_verilog_sva_sequence)
+    {
+      // Same as a ∧ b if the expression is not a sequence.
+      auto lhs = is_state_predicate(sva_and.lhs());
+      auto rhs = is_state_predicate(sva_and.rhs());
+
+      if(lhs.has_value() && rhs.has_value())
+        expr = sva_boolean_exprt{and_exprt{*lhs, *rhs}, expr.type()};
+    }
+    else
+    {
+      expr = and_exprt{sva_and.lhs(), sva_and.rhs()};
+    }
   }
   else if(expr.id() == ID_sva_or)
   {
     auto &sva_or = to_sva_or_expr(expr);
 
-    // Same as a ∨ b if the expression is not a sequence.
-    auto lhs = is_state_formula(sva_or.lhs());
-    auto rhs = is_state_formula(sva_or.rhs());
-
-    if(lhs.has_value() && rhs.has_value())
-      expr = or_exprt{*lhs, *rhs};
+    // can be sequence or property
+    if(expr.type().id() == ID_verilog_sva_sequence)
+    {
+      // Same as a ∨ b if the expression is not a sequence.
+      auto lhs = is_state_predicate(sva_or.lhs());
+      auto rhs = is_state_predicate(sva_or.rhs());
+
+      if(lhs.has_value() && rhs.has_value())
+        expr = sva_boolean_exprt{or_exprt{*lhs, *rhs}, expr.type()};
+    }
+    else
+    {
+      expr = or_exprt{sva_or.lhs(), sva_or.rhs()};
+    }
   }
   else if(expr.id() == ID_sva_not)
   {
-    // Same as regular 'not'. These do not apply to sequences.
+    // Same as boolean 'not'. These do not apply to sequences.
     expr = not_exprt{to_sva_not_expr(expr).op()};
   }
   else if(expr.id() == ID_sva_if)
@@ -113,9 +127,10 @@ exprt trivial_sva(exprt expr)
   {
     // We simplify sequences to boolean expressions, and hence can drop
     // the sva_sequence_property converter
-    auto &op = to_sva_sequence_property_expr_base(expr).sequence();
-    if(op.type().id() == ID_bool)
-      return op;
+    auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
+    auto pred_opt = is_state_predicate(sequence);
+    if(pred_opt.has_value())
+      return *pred_opt;
   }
 
   return expr;
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index 713ef916..2134802a 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -537,10 +537,10 @@ static obligationst property_obligations_rec(
     return property_obligations_rec(
       to_typecast_expr(property_expr).op(), current, no_timeframes);
   }
-  else if(property_expr.id() == ID_not)
+  else if(property_expr.id() == ID_sva_not)
   {
     // We need NNF, try to eliminate the negation.
-    auto &op = to_not_expr(property_expr).op();
+    auto &op = to_sva_not_expr(property_expr).op();
 
     auto op_negated_opt = negate_property_node(op);
 
@@ -576,8 +576,9 @@ static obligationst property_obligations_rec(
     else
     {
       // state formula
-      return obligationst{
-        instantiate_property(property_expr, current, no_timeframes)};
+      auto sampled =
+        instantiate_property(not_exprt{op}, current, no_timeframes);
+      return obligationst{sampled};
     }
   }
   else if(property_expr.id() == ID_sva_implies)
diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp
index 38cf47d5..41464cfc 100644
--- a/src/trans-word-level/sequence.cpp
+++ b/src/trans-word-level/sequence.cpp
@@ -454,10 +454,16 @@ sequence_matchest instantiate_sequence(
 
     return result;
   }
-  else
+  else if(expr.id() == ID_sva_boolean)
   {
-    // not a sequence, evaluate as state predicate
-    auto instantiated = instantiate_property(expr, t, no_timeframes);
+    // a state predicate
+    auto &predicate = to_sva_boolean_expr(expr).op();
+    auto instantiated = instantiate_property(predicate, t, no_timeframes);
     return {{instantiated.first, instantiated.second}};
   }
+  else
+  {
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      false, "unexpected sequence expression", expr.pretty());
+  }
 }
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index 2bdd4060..c9a0ec2c 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -1815,6 +1815,12 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return convert_rec(to_sva_sequence_property_expr_base(src).sequence());
   }
 
+  else if(src.id() == ID_sva_boolean)
+  {
+    // These are invisible
+    return convert_rec(to_sva_boolean_expr(src).op());
+  }
+
   else if(src.id()==ID_sva_sequence_concatenation)
     return convert_sva_sequence_concatenation(
       to_binary_expr(src), precedence = verilog_precedencet::MIN);
diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp
index ce553089..65450192 100644
--- a/src/verilog/sva_expr.cpp
+++ b/src/verilog/sva_expr.cpp
@@ -118,7 +118,9 @@ exprt sva_sequence_repetition_star_exprt::lower() const
     {
       auto n_expr = from_integer(n, integer_typet{});
       result = sva_or_exprt{
-        std::move(result), sva_sequence_repetition_star_exprt{op(), n_expr}};
+        std::move(result),
+        sva_sequence_repetition_star_exprt{op(), n_expr},
+        verilog_sva_sequence_typet{}};
     }
 
     return result;
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
index 22f4746a..694c062e 100644
--- a/src/verilog/sva_expr.h
+++ b/src/verilog/sva_expr.h
@@ -13,12 +13,39 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "verilog_types.h"
 
+/// 1800-2017 16.6 Boolean expressions
+/// Conversion of a Boolean expression into a sequence or property
+class sva_boolean_exprt : public unary_exprt
+{
+public:
+  sva_boolean_exprt(exprt condition, typet __type)
+    : unary_exprt(ID_sva_boolean, std::move(condition), std::move(__type))
+  {
+  }
+};
+
+static inline const sva_boolean_exprt &to_sva_boolean_expr(const exprt &expr)
+{
+  sva_boolean_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_boolean_exprt &>(expr);
+}
+
+static inline sva_boolean_exprt &to_sva_boolean_expr(exprt &expr)
+{
+  sva_boolean_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_boolean_exprt &>(expr);
+}
+
 /// accept_on, reject_on, sync_accept_on, sync_reject_on, disable_iff
-class sva_abort_exprt : public binary_predicate_exprt
+class sva_abort_exprt : public binary_exprt
 {
 public:
   sva_abort_exprt(irep_idt id, exprt condition, exprt property)
-    : binary_predicate_exprt(std::move(condition), id, std::move(property))
+    : binary_exprt(
+        std::move(condition),
+        id,
+        std::move(property),
+        verilog_sva_property_typet{})
   {
   }
 
@@ -43,8 +70,8 @@ class sva_abort_exprt : public binary_predicate_exprt
   }
 
 protected:
-  using binary_predicate_exprt::op0;
-  using binary_predicate_exprt::op1;
+  using binary_exprt::op0;
+  using binary_exprt::op1;
 };
 
 static inline const sva_abort_exprt &to_sva_abort_expr(const exprt &expr)
@@ -87,11 +114,11 @@ static inline sva_disable_iff_exprt &to_sva_disable_iff_expr(exprt &expr)
 }
 
 /// nonindexed variant
-class sva_nexttime_exprt : public unary_predicate_exprt
+class sva_nexttime_exprt : public unary_exprt
 {
 public:
   explicit sva_nexttime_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_nexttime, std::move(op))
+    : unary_exprt(ID_sva_nexttime, std::move(op), verilog_sva_property_typet{})
   {
   }
 };
@@ -111,11 +138,14 @@ static inline sva_nexttime_exprt &to_sva_nexttime_expr(exprt &expr)
 }
 
 /// nonindexed variant
-class sva_s_nexttime_exprt : public unary_predicate_exprt
+class sva_s_nexttime_exprt : public unary_exprt
 {
 public:
   explicit sva_s_nexttime_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_s_nexttime, std::move(op))
+    : unary_exprt(
+        ID_sva_s_nexttime,
+        std::move(op),
+        verilog_sva_property_typet{})
   {
   }
 };
@@ -136,14 +166,15 @@ static inline sva_s_nexttime_exprt &to_sva_s_nexttime_expr(exprt &expr)
 }
 
 /// indexed variant of sva_nexttime_exprt
-class sva_indexed_nexttime_exprt : public binary_predicate_exprt
+class sva_indexed_nexttime_exprt : public binary_exprt
 {
 public:
   sva_indexed_nexttime_exprt(constant_exprt index, exprt op)
-    : binary_predicate_exprt(
+    : binary_exprt(
         std::move(index),
         ID_sva_indexed_nexttime,
-        std::move(op))
+        std::move(op),
+        verilog_sva_property_typet{})
   {
   }
 
@@ -168,8 +199,8 @@ class sva_indexed_nexttime_exprt : public binary_predicate_exprt
   }
 
 protected:
-  using binary_predicate_exprt::op0;
-  using binary_predicate_exprt::op1;
+  using binary_exprt::op0;
+  using binary_exprt::op1;
 };
 
 static inline const sva_indexed_nexttime_exprt &
@@ -189,14 +220,15 @@ to_sva_indexed_nexttime_expr(exprt &expr)
 }
 
 /// indexed variant of sva_s_nexttime_exprt
-class sva_indexed_s_nexttime_exprt : public binary_predicate_exprt
+class sva_indexed_s_nexttime_exprt : public binary_exprt
 {
 public:
   sva_indexed_s_nexttime_exprt(constant_exprt index, exprt op)
-    : binary_predicate_exprt(
+    : binary_exprt(
         std::move(index),
         ID_sva_indexed_s_nexttime,
-        std::move(op))
+        std::move(op),
+        verilog_sva_property_typet{})
   {
   }
 
@@ -221,8 +253,8 @@ class sva_indexed_s_nexttime_exprt : public binary_predicate_exprt
   }
 
 protected:
-  using binary_predicate_exprt::op0;
-  using binary_predicate_exprt::op1;
+  using binary_exprt::op0;
+  using binary_exprt::op1;
 };
 
 static inline const sva_indexed_s_nexttime_exprt &
@@ -257,7 +289,7 @@ class sva_ranged_predicate_exprt : public ternary_exprt
         std::move(__lower),
         std::move(__upper),
         std::move(__op),
-        bool_typet{})
+        verilog_sva_property_typet{})
   {
   }
 
@@ -358,11 +390,14 @@ static inline sva_eventually_exprt &to_sva_eventually_expr(exprt &expr)
   return static_cast<sva_eventually_exprt &>(expr);
 }
 
-class sva_s_eventually_exprt : public unary_predicate_exprt
+class sva_s_eventually_exprt : public unary_exprt
 {
 public:
   explicit sva_s_eventually_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_s_eventually, std::move(op))
+    : unary_exprt(
+        ID_sva_s_eventually,
+        std::move(op),
+        verilog_sva_property_typet{})
   {
   }
 };
@@ -414,11 +449,11 @@ to_sva_ranged_s_eventually_expr(exprt &expr)
   return static_cast<sva_ranged_s_eventually_exprt &>(expr);
 }
 
-class sva_always_exprt : public unary_predicate_exprt
+class sva_always_exprt : public unary_exprt
 {
 public:
   explicit sva_always_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_always, std::move(op))
+    : unary_exprt(ID_sva_always, std::move(op), verilog_sva_property_typet{})
   {
   }
 };
@@ -492,11 +527,11 @@ static inline sva_s_always_exprt &to_sva_s_always_expr(exprt &expr)
   return static_cast<sva_s_always_exprt &>(expr);
 }
 
-class sva_cover_exprt : public unary_predicate_exprt
+class sva_cover_exprt : public unary_exprt
 {
 public:
   explicit sva_cover_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_cover, std::move(op))
+    : unary_exprt(ID_sva_cover, std::move(op), verilog_sva_property_typet{})
   {
   }
 };
@@ -515,11 +550,11 @@ static inline sva_cover_exprt &to_sva_cover_expr(exprt &expr)
   return static_cast<sva_cover_exprt &>(expr);
 }
 
-class sva_assume_exprt : public unary_predicate_exprt
+class sva_assume_exprt : public unary_exprt
 {
 public:
   explicit sva_assume_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_assume, std::move(op))
+    : unary_exprt(ID_sva_assume, std::move(op), verilog_sva_property_typet{})
   {
   }
 };
@@ -538,11 +573,15 @@ static inline sva_assume_exprt &to_sva_assume_expr(exprt &expr)
   return static_cast<sva_assume_exprt &>(expr);
 }
 
-class sva_until_exprt : public binary_predicate_exprt
+class sva_until_exprt : public binary_exprt
 {
 public:
   explicit sva_until_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_sva_until, std::move(op1))
+    : binary_exprt(
+        std::move(op0),
+        ID_sva_until,
+        std::move(op1),
+        verilog_sva_property_typet{})
   {
   }
 };
@@ -561,11 +600,15 @@ static inline sva_until_exprt &to_sva_until_expr(exprt &expr)
   return static_cast<sva_until_exprt &>(expr);
 }
 
-class sva_s_until_exprt : public binary_predicate_exprt
+class sva_s_until_exprt : public binary_exprt
 {
 public:
   explicit sva_s_until_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_sva_s_until, std::move(op1))
+    : binary_exprt(
+        std::move(op0),
+        ID_sva_s_until,
+        std::move(op1),
+        verilog_sva_property_typet{})
   {
   }
 };
@@ -585,11 +628,15 @@ static inline sva_s_until_exprt &to_sva_s_until_expr(exprt &expr)
 }
 
 /// SVA until_with operator -- like LTL (weak) R, but lhs/rhs swapped
-class sva_until_with_exprt : public binary_predicate_exprt
+class sva_until_with_exprt : public binary_exprt
 {
 public:
   explicit sva_until_with_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_sva_until_with, std::move(op1))
+    : binary_exprt(
+        std::move(op0),
+        ID_sva_until_with,
+        std::move(op1),
+        verilog_sva_property_typet{})
   {
   }
 };
@@ -610,14 +657,15 @@ static inline sva_until_with_exprt &to_sva_until_with_expr(exprt &expr)
 }
 
 /// SVA s_until_with operator -- like LTL strong R, but lhs/rhs swapped
-class sva_s_until_with_exprt : public binary_predicate_exprt
+class sva_s_until_with_exprt : public binary_exprt
 {
 public:
   explicit sva_s_until_with_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(
+    : binary_exprt(
         std::move(op0),
         ID_sva_s_until_with,
-        std::move(op1))
+        std::move(op1),
+        verilog_sva_property_typet{})
   {
   }
 };
@@ -638,17 +686,18 @@ static inline sva_s_until_with_exprt &to_sva_s_until_with_expr(exprt &expr)
 }
 
 /// base class for |->, |=>, #-#, #=#
-class sva_implication_base_exprt : public binary_predicate_exprt
+class sva_implication_base_exprt : public binary_exprt
 {
 public:
   explicit sva_implication_base_exprt(
     exprt __antecedent,
     irep_idt __id,
     exprt __consequent)
-    : binary_predicate_exprt(
+    : binary_exprt(
         std::move(__antecedent),
         __id,
-        std::move(__consequent))
+        std::move(__consequent),
+        verilog_sva_property_typet{})
   {
   }
 
@@ -771,11 +820,11 @@ to_sva_non_overlapped_implication_expr(exprt &expr)
   return static_cast<sva_non_overlapped_implication_exprt &>(expr);
 }
 
-class sva_not_exprt : public unary_predicate_exprt
+class sva_not_exprt : public unary_exprt
 {
 public:
   explicit sva_not_exprt(exprt op)
-    : unary_predicate_exprt(ID_sva_not, std::move(op))
+    : unary_exprt(ID_sva_not, std::move(op), verilog_sva_property_typet{})
   {
   }
 };
@@ -794,11 +843,16 @@ static inline sva_not_exprt &to_sva_not_expr(exprt &expr)
   return static_cast<sva_not_exprt &>(expr);
 }
 
-class sva_and_exprt : public binary_predicate_exprt
+class sva_and_exprt : public binary_exprt
 {
 public:
-  explicit sva_and_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_sva_and, std::move(op1))
+  // can be a sequence or property, depending on operands
+  explicit sva_and_exprt(exprt op0, exprt op1, typet __type)
+    : binary_exprt(
+        std::move(op0),
+        ID_sva_and,
+        std::move(op1),
+        std::move(__type))
   {
   }
 };
@@ -846,11 +900,15 @@ to_sva_sequence_concatenation_expr(exprt &expr)
   return static_cast<sva_sequence_concatenation_exprt &>(expr);
 }
 
-class sva_iff_exprt : public binary_predicate_exprt
+class sva_iff_exprt : public binary_exprt
 {
 public:
   explicit sva_iff_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_sva_iff, std::move(op1))
+    : binary_exprt(
+        std::move(op0),
+        ID_sva_iff,
+        std::move(op1),
+        verilog_sva_property_typet{})
   {
   }
 };
@@ -869,11 +927,15 @@ static inline sva_iff_exprt &to_sva_iff_expr(exprt &expr)
   return static_cast<sva_iff_exprt &>(expr);
 }
 
-class sva_implies_exprt : public binary_predicate_exprt
+class sva_implies_exprt : public binary_exprt
 {
 public:
   explicit sva_implies_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_sva_implies, std::move(op1))
+    : binary_exprt(
+        std::move(op0),
+        ID_sva_implies,
+        std::move(op1),
+        verilog_sva_property_typet{})
   {
   }
 };
@@ -892,11 +954,12 @@ static inline sva_implies_exprt &to_sva_implies_expr(exprt &expr)
   return static_cast<sva_implies_exprt &>(expr);
 }
 
-class sva_or_exprt : public binary_predicate_exprt
+class sva_or_exprt : public binary_exprt
 {
 public:
-  explicit sva_or_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(std::move(op0), ID_sva_or, std::move(op1))
+  // These can be sequences or properties, depending on the operands
+  explicit sva_or_exprt(exprt op0, exprt op1, typet __type)
+    : binary_exprt(std::move(op0), ID_sva_or, std::move(op1), std::move(__type))
   {
   }
 };
@@ -1103,7 +1166,7 @@ class sva_if_exprt : public ternary_exprt
         std::move(__cond),
         std::move(__true_case),
         std::move(__false_case),
-        bool_typet())
+        verilog_sva_property_typet{})
   {
   }
 
@@ -1160,11 +1223,11 @@ static inline sva_if_exprt &to_sva_if_expr(exprt &expr)
 
 /// Base class for sequence property expressions.
 /// 1800-2017 16.12.2 Sequence property
-class sva_sequence_property_expr_baset : public unary_predicate_exprt
+class sva_sequence_property_expr_baset : public unary_exprt
 {
 public:
   sva_sequence_property_expr_baset(irep_idt __id, exprt __op)
-    : unary_predicate_exprt(__id, std::move(__op))
+    : unary_exprt(__id, std::move(__op), verilog_sva_property_typet{})
   {
   }
 
@@ -1179,7 +1242,7 @@ class sva_sequence_property_expr_baset : public unary_predicate_exprt
   }
 
 protected:
-  using unary_predicate_exprt::op;
+  using unary_exprt::op;
 };
 
 inline const sva_sequence_property_expr_baset &
@@ -1244,14 +1307,15 @@ inline sva_weak_exprt &to_sva_weak_expr(exprt &expr)
   return static_cast<sva_weak_exprt &>(expr);
 }
 
-class sva_case_exprt : public binary_predicate_exprt
+class sva_case_exprt : public binary_exprt
 {
 public:
   explicit sva_case_exprt(exprt __case_op, exprt __cases)
-    : binary_predicate_exprt(
+    : binary_exprt(
         std::move(__case_op),
         ID_sva_case,
-        std::move(__cases))
+        std::move(__cases),
+        verilog_sva_property_typet{})
   {
   }
 
@@ -1308,8 +1372,8 @@ class sva_case_exprt : public binary_predicate_exprt
   exprt lowering() const;
 
 protected:
-  using binary_predicate_exprt::op0;
-  using binary_predicate_exprt::op1;
+  using binary_exprt::op0;
+  using binary_exprt::op1;
 };
 
 inline const sva_case_exprt &to_sva_case_expr(const exprt &expr)
diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp
index f0dd53fd..d7b42b5c 100644
--- a/src/verilog/verilog_typecheck_sva.cpp
+++ b/src/verilog/verilog_typecheck_sva.cpp
@@ -35,10 +35,16 @@ void verilog_typecheck_exprt::require_sva_sequence(exprt &expr)
     }
     else
     {
-      // state formula, can cast to sequence
+      // state formula, can convert to sequence
       make_boolean(expr);
+      expr = sva_boolean_exprt{std::move(expr), verilog_sva_sequence_typet{}};
     }
   }
+  else if(type.id() == ID_verilog_sva_property)
+  {
+    throw errort().with_location(expr.source_location())
+      << "sequence required, but got property";
+  }
   else
   {
     throw errort().with_location(expr.source_location())
@@ -58,6 +64,10 @@ void verilog_typecheck_exprt::require_sva_property(exprt &expr)
     // or cover.
     expr = sva_sequence_property_exprt{std::move(expr)};
   }
+  else if(type.id() == ID_verilog_sva_property)
+  {
+    // good as is
+  }
   else if(
     type.id() == ID_bool || type.id() == ID_unsignedbv ||
     type.id() == ID_signedbv || type.id() == ID_verilog_unsignedbv ||
@@ -82,7 +92,7 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr)
   {
     convert_sva(expr.op());
     require_sva_property(expr.op());
-    expr.type() = bool_typet{}; // always boolean, never x
+    expr.type() = verilog_sva_property_typet{}; // always boolean, never x
     return std::move(expr);
   }
   else if(
@@ -99,7 +109,7 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr)
   {
     convert_sva(expr.op());
     require_sva_sequence(expr.op());
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
     return std::move(expr);
   }
   else
@@ -133,7 +143,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
       require_sva_property(expr.lhs());
       require_sva_property(expr.rhs());
       // always boolean, never x
-      expr.type() = bool_typet{};
+      expr.type() = verilog_sva_property_typet{};
     }
 
     return std::move(expr);
@@ -147,7 +157,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
     require_sva_property(expr.rhs());
 
     // always boolean, never x
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
 
     return std::move(expr);
   }
@@ -163,7 +173,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
 
     convert_sva(to_sva_abort_expr(expr).property());
     require_sva_property(to_sva_abort_expr(expr).property());
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
 
     return std::move(expr);
   }
@@ -174,7 +184,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
     auto &op = to_sva_indexed_nexttime_expr(expr).op();
     convert_sva(op);
     require_sva_property(op);
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
 
     return std::move(expr);
   }
@@ -185,7 +195,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
     auto &op = to_sva_indexed_s_nexttime_expr(expr).op();
     convert_sva(op);
     require_sva_property(op);
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
 
     return std::move(expr);
   }
@@ -204,7 +214,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
     convert_sva(expr.rhs());
     require_sva_property(expr.rhs());
 
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
     return std::move(expr);
   }
   else if(
@@ -217,7 +227,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
     convert_sva(expr.rhs());
     require_sva_property(expr.rhs());
 
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
 
     return std::move(expr);
   }
@@ -285,7 +295,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
       require_sva_property(case_item.result());
     }
 
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
     return std::move(expr);
   }
   else
@@ -395,7 +405,7 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
 
     convert_sva(expr.op2());
     require_sva_property(expr.op2());
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
 
     return std::move(expr);
   }
@@ -414,7 +424,7 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
     }
 
     // These are always property expressions
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
 
     return std::move(expr);
   }
diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h
index b3d8aec7..5c5916d7 100644
--- a/src/verilog/verilog_types.h
+++ b/src/verilog/verilog_types.h
@@ -739,6 +739,15 @@ inline verilog_package_scope_typet &to_verilog_package_scope_type(typet &type)
   return static_cast<verilog_package_scope_typet &>(type);
 }
 
+/// SVA properties
+class verilog_sva_property_typet : public typet
+{
+public:
+  verilog_sva_property_typet() : typet(ID_verilog_sva_property)
+  {
+  }
+};
+
 /// SVA sequences
 class verilog_sva_sequence_typet : public typet
 {