diff --git a/regression/ebmc/smv-netlist/always_with_range1.desc b/regression/ebmc/smv-netlist/always_with_range1.desc
index 296eb319f..1f123a9a7 100644
--- a/regression/ebmc/smv-netlist/always_with_range1.desc
+++ b/regression/ebmc/smv-netlist/always_with_range1.desc
@@ -4,7 +4,7 @@ always_with_range1.sv
 ^LTLSPEC node275 & X node275 & X X node275 .*
 ^LTLSPEC G node275$
 ^LTLSPEC node275 & X node275 & X X node275 .*
-^LTLSPEC G \(\!node306 \| X node337\)$
+^LTLSPEC G \(X node306 -> node337\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index c2f4ddd0d..8d37e95fe 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -147,6 +147,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/sva_to_ltl.cpp b/src/temporal-logic/sva_to_ltl.cpp
index 97341b712..00e4cbb9f 100644
--- a/src/temporal-logic/sva_to_ltl.cpp
+++ b/src/temporal-logic/sva_to_ltl.cpp
@@ -238,6 +238,38 @@ exprt SVA_to_LTL(exprt expr)
   {
     return expr;
   }
+  else if(expr.id() == ID_sva_implies)
+  {
+    // maps cleanly to 'implies'
+    auto &sva_implies = to_sva_implies_expr(expr);
+    auto rec_lhs = SVA_to_LTL(sva_implies.lhs());
+    auto rec_rhs = SVA_to_LTL(sva_implies.rhs());
+    return implies_exprt{rec_rhs, rec_lhs};
+  }
+  else if(expr.id() == ID_sva_iff)
+  {
+    // maps cleanly to =
+    auto &sva_iff = to_sva_iff_expr(expr);
+    auto rec_lhs = SVA_to_LTL(sva_iff.lhs());
+    auto rec_rhs = SVA_to_LTL(sva_iff.rhs());
+    return equal_exprt{rec_rhs, rec_lhs};
+  }
+  else if(expr.id() == ID_sva_and)
+  {
+    // maps cleanly to Boolean and
+    auto &sva_iff = to_sva_iff_expr(expr);
+    auto rec_lhs = SVA_to_LTL(sva_iff.lhs());
+    auto rec_rhs = SVA_to_LTL(sva_iff.rhs());
+    return and_exprt{rec_rhs, rec_lhs};
+  }
+  else if(expr.id() == ID_sva_or)
+  {
+    // maps cleanly to Boolean or
+    auto &sva_iff = to_sva_iff_expr(expr);
+    auto rec_lhs = SVA_to_LTL(sva_iff.lhs());
+    auto rec_rhs = SVA_to_LTL(sva_iff.rhs());
+    return or_exprt{rec_rhs, rec_lhs};
+  }
   else if(
     expr.id() == ID_and || expr.id() == ID_implies || expr.id() == ID_or ||
     expr.id() == ID_not)
diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp
index 223ab386d..7b9b2d28a 100644
--- a/src/verilog/sva_expr.cpp
+++ b/src/verilog/sva_expr.cpp
@@ -11,6 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/mathematical_types.h>
 
+exprt sva_iff_exprt::implications() const
+{
+  return sva_and_exprt{
+    sva_implies_exprt{lhs(), rhs()}, sva_implies_exprt{rhs(), lhs()}, type()};
+}
+
 exprt sva_cycle_delay_plus_exprt::lower() const
 {
   // same as ##[1:$]
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
index 9b3f68a2e..b9ad4a993 100644
--- a/src/verilog/sva_expr.h
+++ b/src/verilog/sva_expr.h
@@ -37,11 +37,15 @@ static inline sva_boolean_exprt &to_sva_boolean_expr(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{})
   {
   }
 
@@ -66,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)
@@ -110,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{})
   {
   }
 };
@@ -134,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{})
   {
   }
 };
@@ -159,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{})
   {
   }
 
@@ -191,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 &
@@ -212,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{})
   {
   }
 
@@ -244,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 &
@@ -280,7 +289,7 @@ class sva_ranged_predicate_exprt : public ternary_exprt
         std::move(__from),
         std::move(__to),
         std::move(__op),
-        bool_typet{})
+        verilog_sva_property_typet{})
   {
   }
 
@@ -402,11 +411,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{})
   {
   }
 };
@@ -458,11 +470,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{})
   {
   }
 };
@@ -536,11 +548,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{})
   {
   }
 };
@@ -559,11 +571,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{})
   {
   }
 };
@@ -582,11 +594,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{})
   {
   }
 };
@@ -605,11 +621,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{})
   {
   }
 };
@@ -629,11 +649,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{})
   {
   }
 };
@@ -654,14 +678,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{})
   {
   }
 };
@@ -682,17 +707,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{})
   {
   }
 
@@ -815,11 +841,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{})
   {
   }
 };
@@ -841,8 +867,13 @@ static inline sva_not_exprt &to_sva_not_expr(exprt &expr)
 class sva_and_exprt : public binary_exprt
 {
 public:
-  explicit sva_and_exprt(exprt op0, exprt op1, typet type)
-    : binary_exprt(std::move(op0), ID_sva_and, std::move(op1), std::move(type))
+  // 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))
   {
   }
 };
@@ -861,13 +892,20 @@ static inline sva_and_exprt &to_sva_and_expr(exprt &expr)
   return static_cast<sva_and_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{})
   {
   }
+
+  // (lhs implies rhs) and (rhs implies lhs)
+  exprt implications() const;
 };
 
 static inline const sva_iff_exprt &to_sva_iff_expr(const exprt &expr)
@@ -884,11 +922,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{})
   {
   }
 };
@@ -910,8 +952,9 @@ static inline sva_implies_exprt &to_sva_implies_expr(exprt &expr)
 class sva_or_exprt : public binary_exprt
 {
 public:
-  explicit sva_or_exprt(exprt op0, exprt op1, typet type)
-    : binary_exprt(std::move(op0), ID_sva_or, std::move(op1), std::move(type))
+  // 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))
   {
   }
 };
@@ -1143,7 +1186,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{})
   {
   }
 
@@ -1200,11 +1243,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{})
   {
   }
 
@@ -1219,7 +1262,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 &
@@ -1284,14 +1327,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{})
   {
   }
 
@@ -1348,8 +1392,8 @@ class sva_case_exprt : public binary_predicate_exprt
   exprt lower() 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_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 465869999..9da413a85 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -51,6 +51,10 @@ typet verilog_lowering(typet type)
   {
     return to_verilog_event_type(type).encoding();
   }
+  else if(type.id() == ID_verilog_sva_property)
+  {
+    return bool_typet{};
+  }
   else
     return type;
 }
diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp
index 29e21bde9..4efb9f99b 100644
--- a/src/verilog/verilog_typecheck_sva.cpp
+++ b/src/verilog/verilog_typecheck_sva.cpp
@@ -42,6 +42,11 @@ void verilog_typecheck_exprt::require_sva_sequence(exprt &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())
@@ -61,6 +66,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 ||
@@ -85,14 +94,14 @@ 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(expr.id() == ID_sva_weak || expr.id() == ID_sva_strong)
   {
     convert_sva(expr.op());
     require_sva_sequence(expr.op());
-    expr.type() = bool_typet{};
+    expr.type() = verilog_sva_property_typet{};
     return std::move(expr);
   }
   else
@@ -126,7 +135,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);
@@ -140,7 +149,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);
   }
@@ -156,7 +165,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);
   }
@@ -185,7 +194,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);
   }
@@ -196,7 +205,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);
   }
@@ -215,7 +224,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(
@@ -228,7 +237,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);
   }
@@ -295,7 +304,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
@@ -387,7 +396,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);
   }
@@ -406,7 +415,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 b3d8aec77..5c5916d77 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
 {